\documentclass[AMA,STIX1COL]{WileyNJD-v2}

\articletype{Research Article}

\received{26 April 2016}
\revised{6 June 2016}
\accepted{6 June 2016}

%\raggedbottom

%\usepackage{booktabs}

\let\procedure\relax
\let\endprocedure\relax

%\usepackage[ruled]{algorithm2e} % For algorithms

\usepackage[noline, noend, nofillcomment, linesnumbered]{algorithm2e}
%\usepackage[noline, noend, nofillcomment]{algorithm2e}
%\usepackage[noline, noend, nofillcomment, linesnumbered]{algorithm2e}
%    \setlength{\algomargin}{0em}

\usepackage{setspace}

\SetArgSty{textnormal}

% comments in the pseudocode
% note: on my sistem \texttt is broken with \small font size (too small)
\newcommand\Xcommentfont[1]{\selectfont\textnormal{#1}}
%\newcommand\Xcommentfont[1]{\fontsize{9pt}{0pt}\selectfont\texttt{#1}}
\SetCommentSty{Xcommentfont}
\SetNoFillComment

\SetNlSty{textnormal}{}{}

\renewcommand{\algorithmcfname}{ALGORITHM}
%\SetAlFnt{\small}
%\SetAlCapFnt{\small}
%\SetAlCapNameFnt{\small}
%\SetAlCapHSkip{0pt}
\IncMargin{-\parindent}

\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{accents}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{enumitem}
\usepackage[justification=centering]{caption}
\usepackage{url}
\usepackage[section]{placeins}

\newcommand{\Xl}{\langle}
\newcommand{\Xr}{\rangle}
\newcommand{\Xm}{\langle\!\rangle}
\newcommand{\Xset}{\!\leftarrow\!}
\newcommand{\Xund}{\rule{.4em}{.4pt}}
\newcommand{\Xlb}{[\![}
\newcommand{\Xrb}{]\!]}
\newcommand{\Xmap}{\!\mapsto\!}
\newcommand{\XB}{\mathcal{B}}
\newcommand{\XD}{\mathcal{D}}
\newcommand{\XE}{\mathcal{E}}
\newcommand{\XF}{\mathcal{F}}
\newcommand{\XI}{\mathcal{I}}
\newcommand{\XIT}{\XI\!\XT}
\newcommand{\XIR}{\XI\!\XR}
\newcommand{\XL}{\mathcal{L}}
\newcommand{\XN}{\mathcal{N}}
\newcommand{\XM}{\mathcal{M}}
\newcommand{\XO}{\mathcal{O}}
\newcommand{\XP}{\mathcal{P}}
\newcommand{\XR}{\mathcal{R}}
\newcommand{\XS}{\mathcal{S}}
\newcommand{\XT}{\mathcal{T}}
\newcommand{\XX}{\mathcal{X}}
\newcommand{\YB}{\mathbb{B}}
\newcommand{\YC}{\mathbb{C}}
\newcommand{\YF}{\mathbb{F}}
\newcommand{\YN}{\mathbb{N}}
\newcommand{\YT}{\mathbb{T}}
\newcommand{\YQ}{\mathbb{Q}}
\newcommand{\YZ}{\mathbb{Z}}
\newcommand{\IPT}{I\!PT}
\newcommand{\IRE}{I\!RE}

\newcommand{\Xstirling}[2]{\genfrac{\{}{\}}{0pt}{}{#1}{#2}}
\newcommand*{\Xbar}[1]{\overline{#1\vphantom{\bar{#1}}}}
\newcommand{\pnorm}[2]{\|{#1}\|^{Pos}_{#2}}
\newcommand{\snorm}[2]{\|{#1}\|^{Sub}_{#2}}

\setlist{nosep}
%\setlength{\parskip}{0.5em}

\newenvironment{Xfig}
    {\par\medskip\noindent\minipage{\linewidth}\begin{center}}
    {\end{center}\endminipage\par\medskip}
\newenvironment{Xtab}
    {\par\medskip\noindent\minipage{\linewidth}\begin{center}}
    {\end{center}\endminipage\par\medskip}

%\setlength{\parindent}{0pt}

%\theoremstyle{definition}
\newtheorem{Xdef}{Definition}
\newtheorem{XThe}{Theorem}
\newtheorem{XLem}{Lemma}
\newtheorem{Xobs}{Observation}


\begin{document}

\title{POSIX Disambiguation on Tagged NFA}

\author[1]{Angelo Borsotti}
\author[2]{Ulya Trofimovich}

\address[1]{\email{angelo.borsotti@mail.polimi.it}}
\address[2]{\email{skvadrik@gmail.com}}

\abstract[Summary]{
We give an algorithm for POSIX submatch extraction in regular expressions.
Our work is based on the prior work of Okui and Suzuki, with a number of improvements.
First, the new algorithm can handle bounded repetition.
Second, it explores only a part of the regular expression structure
necessary to disambiguate submatch extraction,
which reduces the overhead for expressions with few submatch groups.
Third, we use Thompson automata instead of position automata
and give an efficient algorithm for $\epsilon$-closure construction,
which allows us to skip the pre-processing step of Okui-Suzuki algorithm.
%based on the Goldberg-Radzik shortest path finding algorithm.
The complexity of our algorithm is $O(nv^2e)$ in general and $O(nve)$ for regular expression without $\epsilon$-loops,
where $n$ is the input length, $v$ is the number of states and $e$ is the number of transitions in the automaton.
}

\keywords{Lexical Analysis, Regular Expressions, Submatch Extraction, POSIX}

%\jnlcitation{\cname{
%\author{U. Trofimovich},
%(\cyear{2017}),
%\ctitle{Fast Submatch Extraction in Lexer Generators},
%\cjournal{Q.J.R. Meteorol. Soc.},
%\cvol{2017;00:1--6}.}

\maketitle

\section*{Introduction}

\iffalse

     Yes, I know --- you've always been after building full parse trees,


This is true, but the issue here is different. It is a matter of RE syntax and its interpretation.
As you know, there are two views of REs: the one of Kleene (the theoretical computer science one), and the
one of RE libraries. The first  (see Kleene, Stephen C. (1951). Shannon, Claude E.; McCarthy, John, eds.
Representation of Events in Nerve Nets and Finite Automata (PDF). Automata Studies. Princeton University
Press. pp. 3–42) has no notion of submatches and capturing parentheses. Indeed, parentheses in it
are seen as in math, i.e. having no other significance than a means of changing the precedence of
operators. In it then, r* and (r)* are the same.
In the RE libraries view, this could be different. E.g. in the POSIX standard (the first, Chapter 9) the definition
of "matching" (9.4.6) refers always to "ERE matching a single character or an ERE enclosed in parentheses"
making thus no distiction between r* and (r)*. What makes the distinction is the POSIX standard for regex().
Actually, tagged automata depart from regex() since they allow to get the match of any part of a string be it
derived from a capturing group or not.
I think that we can do what we want since we are not presenting a paper that describes an implementation of
regex(). I have no problems in making the distinction; it is a valid choice much the same as the other one.
After all, since we are not describing an implementation of regex(), this distinction does not make much
a difference (apart perhaps a level in the pictures of trees, and some tweaks in the proofs).

\fi

Description of Okui algorithm.
\\ \\
Contributions.
%\begin{itemize}
%    \item
%    \item
%\end{itemize}
\\ \\
The rest of this paper is arranged as follows.

\section{Regular Expressions and Ordered Parse Trees}

In this section we revise the basic definitions of
regular expressions,
parse trees,
ambiguity
and the order on parse trees.

    \begin{Xdef}
    \emph{Regular expressions (REs)} over finite alphabet $\Sigma$, denoted $\XR_\Sigma$, are:
    \begin{enumerate}
        \item Atomic REs:
%          \emph{empty set} $\emptyset \in \XE_\Sigma$,
          \emph{empty word} $\epsilon \in \XR_\Sigma$ and
          \emph{unit word} $\alpha \in \XR_\Sigma$, where $\alpha \in \Sigma$.
        \item Compound REs: if $e_1, e_2 \in \XR_\Sigma$, then
          \emph{union} $e_1 | e_2 \in \XR_\Sigma$,
          \emph{product} $e_1 e_2 \in \XR_\Sigma$,
          \emph{repetition} $e_1^{n, m} \in \XR_\Sigma$ (where $0 \leq n \leq m \leq \infty$), and
          \emph{submatch group} $(e_1) \in \XR_\Sigma$.
    \end{enumerate}
    \end{Xdef}

REs originate in the work of Kleene\cite{Kle51}.
A mathematically rigorous definition of REs is given in terms of the Kleene algebra\cite{Koz94}.
Our definition is close to the one widely used in literature\cite{HU90}\cite{SS88},
with a couple of minor adaptations to the POSIX standard.
First, we consider parentheses as a distinct construct: in POSIX $(e)$ is semantically different from $e$.
Second, we use generalized repetition $e^{n, m}$ instead of iteration $e^*$:
expressing repetition in terms of iteration and product requires duplication of the subexpression,
which may change semantics: e.g. in POSIX $(e)(e)$ is not the same as $(e)^{2,2}$.
As usual, we assume that repetition has precedence over product and product over union,
and parentheses may be used to override it (all parentheses are capturing).
%Additionally, we use the following shortcut notation:
%$e^*$ for $e^{0,\infty}$,
%$e^+$ for $e^{1,\infty}$,
%$e^?$ for $e^{0,1}$,
%and $e^n$ for $e^{n,n}$.
% %\\
% %
% %One possible interpretation of RE is the \emph{tree} interpretation,
% %in which every RE denotes a set of \emph{parse trees}.

    \begin{Xdef}
    \emph{Parse trees (PT)} over finite alphabet $\Sigma$, denoted $\XT_\Sigma$, are:
    \begin{enumerate}
        \item Atomic PT:
          \emph{nil tree} ${\varnothing} \in \XT_\Sigma$,
          \emph{empty tree} ${\epsilon} \in \XT_\Sigma$ and
          \emph{unit tree} ${\alpha} \in \XT_\Sigma$, where $\alpha \in \Sigma$.
        \item Compound PT: if $t_1, \dots, t_n \in \XT_\Sigma$, where $n \geq 1$, then
          ${T}(t_1, \dots, t_n) \in \XT_\Sigma$.
    \end{enumerate}
    \end{Xdef}

Note that our PTs are different from \ref{OS13}:
we have a \emph{nil} tree (a placeholder for absent alternative and zero repetitions)
and do not differentiate between various kinds of compound trees.
Each RE denotes a set of PTs given by the operator $PT: \XR_\Sigma \rightarrow 2^{\XT_\Sigma}$:
    \begin{align*}
        PT(\epsilon) &= \{ {\epsilon} \}
        \\
        PT(\alpha) &= \{ {\alpha} \}
        \\
        PT(r_1 \mid r_2) &=
            \big\{ {T}(t, \varnothing) \mid t \in PT(r_1) \big\} \cup
            \big\{ {T}(\varnothing, t) \mid t \in PT(r_2) \big\}
        \\
        PT(r_1 \cdot r_2) &=
            \big\{ {T}(t_1, t_2) \mid
                t_1 \in PT(r_1),
                t_2 \in PT(r_2)
            \big\} \\
        PT(r^{n, m}) &=
            \begin{cases}
                \big\{ {T}(t_1, \dots, t_m) \mid t_i \in PT(r) \;
                    \forall i = \overline{1, m} \big\} \cup \{ {T}(\varnothing) \} &\text{if } n = 0 \\
                \big\{ {T}(t_n, \dots, t_m) \mid t_i \in PT(r) \;
                    \forall i = \overline{n, m} \big\} &\text{if } n > 0
            \end{cases}
        \\
        PT( (r) ) &= PT(r)
    \end{align*}

The \emph{string} induced by a PT $t$, denoted $str(t)$, is the concatenation of all alphabet symbols in the left-to-right traversal of $t$.
For a RE $r$ and a string $w$, we write $PT(r, w)$ to denote the set $\{ t \in PT(r) \mid str(t) = w \}$
(note that this set is potentially infinite).

    \begin{Xdef}\label{ambiguity_of_parse_trees}
    PTs $s$ and $t$ are \emph{ambiguous} iff $s \neq t$ and $s, t \in PT(r, w)$ for some RE $r$ and string $w$.
    $\square$
    \end{Xdef}

Following \ref{OS13}, we assign \emph{positions} to the nodes of RE and PT.
The root position is $\Lambda$, and position of the $i$-th subtree of a tree with position $p$ is $p.i$.
The \emph{length} of position $p$, denoted $|p|$, is defined as $0$ for $\Lambda$ and $|p| + 1$ for $p.i$.
%The set of all positions is denoted $\XP$.
The subtree of a tree $t$ at position $p$ is denoted $t|_p$.
Position $p$ is a \emph{prefix} of position $q$ iff $q = p.p'$ for some $p'$,
and a \emph{proper prefix} if additionaly $p \neq q$.
Position $p$ is a \emph{sibling} of position $q$ iff $q = q'.i, p = q'.j$ for some $q'$ and $i,j \in \YN$.
Positions are ordered lexicographically, as in \ref{OS13}.
The set of all positions of a tree $t$ is denoted $Pos(t)$.

    \begin{Xdef}\label{norm_of_parse_tree}
    The \emph{norm} of PT $t$ at position $p$ is:
    \begin{align*}
    \|t\|_p &=
        \begin{cases}
            -1          &\text{if } p \in Pos(t) \text{ and } t|_p = \varnothing  \\
            |str(t|_p)| &\text{if } p \in Pos(t) \text{ and } t|_p \neq \varnothing \\
            \infty      &\text{if } p \not\in Pos(t)
        \end{cases}
    \end{align*}
    \end{Xdef}

We shorten $\|t\|_\Lambda$ as $\|t\|$.
Generally the norm of a subtree means the number of alphabet symbols in the leaves of this subtree, with two exceptions.
First, for nil subtrees the norm is $-1$: intuitively, they have the lowest ``ranking'' among all possible subtrees.
Second, for inexistent subtrees (those with positions out of $Pos(t)$) the norm is infinite.
This may seem counterintuitive at first, but it makes sense in the presense of REs with empty repetition.
According to the POSIX standard, optional empty repetitions are not allowed,
and our definition of the norm reflects this:
if a tree $s$ has a subtree $s|_p$ corresponding to an empty repetition,
and another tree $t$ has no subtree at position $p$ ($p \not\in Pos(t)$),
then the infinite norm $\|t\|_p$ ``outranks'' $\|s\|_p$.

    \begin{Xdef}\label{order_on_PTs}
    \emph{Order on PTs.}
    Given parse trees $t, s \in PT(e, w)$, we say that $t <_p s$ w.r.t. \emph{desision position} $p$ % $p \in Sub(t) \cup Sub(s)$
    iff $\|t\|_p > \|s\|_p$ and $\|t\|_q = \|s\|_q \; \forall q < p$.
    We say that $t < s$ iff $t <_p s$ for some $p$.
    \end{Xdef}

Note that in the definition \ref{order_on_PTs}
we do not explicitly demand that $p, q \in Pos(t) \cup Pos(s)$:
if this is not the case, the norms of both subtrees are $\infty$ and thus equal.
Also note that our definition of order differs from the one given by Okui and Suzuki \ref{OS13}:
we define order on the whole set of PTs,
while they defined it on a finite subset of PTs called \emph{canonical parse trees (CPTs)} ---
a subset of PTs that do not contain subtrees corresponding to optional empty repetitions.
We extend their definition to non-canonical PTs.

    \begin{XThe}
    Relation $<$ is a strict total order on PTs.
    \end{XThe}



\section{Partially Ordered Parse Trees}

The POSIX standard uses the terms \emph{subexpression} and \emph{subpattern}
when speaking about parenthesized and non-parenthesized sub-REs respectively.
The difference between them is that
subexpressions (also called \emph{submatch groups}) are subject to submatch extraction:
if a RE matches some string, we need to know what part of the string matches each subexpression.
For subpatterns we don't need this information.
According to the POSIX standard, both subexpressions and subpatterns
obey the same hierarchical rules,
where the outer sub-REs are prior to the inner sub-REs and the left sub-REs are prior to the right sub-REs.
Disambiguation starts with the topmost sub-RE and proceeds down to each most nested subexpression,
considering all prior sub-RE on its way (both subexpressions and subpatterns),
and stopping at the first difference.
%
In order to reflect these disambiguation rules, we introduce the notion of explicit and implicit submatch groups:
\emph{explicit submatch group} is a subexpression
and \emph{implicit submatch group} is either a subexpression, or a subpattern which contains nested or sibling subexpressions.
In this section we rewrite REs in a form
where every sub-RE is equipped with a pair of numbers called
\emph{implicit submatch index} and \emph{explicit submatch index}.
As the reader might guess, these numbers indicate if the given sub-RE is an implicit or explicit submatch group.
%
For a given sub-RE,
if both indices are zero, it means that this sub-RE is ignored from submatch extraction perspective.
If only the second index is zero, it means that the sub-RE itself is not subject to submatch extraction,
but it may be involved in disambiguation.
If both indices are non-zero, then the sub-RE is a submatch group.
%
Indices are convenient because they allow us to consider individual sub-REs
without loosing the submatch context of the whole RE.
We call this representation \emph{indexed regular expressions (IREs)}.
%An example of IRE can be seen on figure \ref{fig_parse_trees}.

    \begin{Xdef}
    \emph{Indexed regular expressions (IREs)} over finite alphabet $\Sigma$, denoted $\XIR_\Sigma$, are:
    \begin{enumerate}
        \item Atomic IREs:
          \emph{empty tree} $(i, j, \epsilon) \in \XIR_\Sigma$ and
          \emph{unit tree} $(i, j, \alpha) \in \XIR_\Sigma$, where $\alpha \in \Sigma$ and $i, j \in \YZ$.

        \item Compound IREs: if $r_1, r_2 \in \XIR_\Sigma$ and $i, j \in \YZ$, then
          \emph{union} $(i, j, r_1 \mid r_2) \in \XIR_\Sigma$,
          \emph{product} $(i, j, r_1 \cdot r_2) \in \XIR_\Sigma$ and
          \emph{repetition} $(i, j, r_1^{n, m}) \in \XIR_\Sigma$ (where $0 \leq n \leq m \leq \infty$).
    \end{enumerate}
    \end{Xdef}

The function $\IRE : \XR_\Sigma \rightarrow \XIR_\Sigma$ transforms REs into IREs.
It is defined via a composition of two functions,
$mark$ that transforms REs into IREs with submatch indices in the boolean range $\{0, 1\}$,
and $enum$ that substitutes boolean indices with consecutive numbers:
$\IRE(e) = r$ where $(\Xund, \Xund, r) = enum(1, 1, mark(e))$.
Note that we consider $(e)$ as a special case of repetition $(e)^{1,1}$:
this allows us to handle all parenthesized sub-RE uniformly.
An example of constructing an IRE from a RE is given on figure \ref{fig_mark_enum}.
The reverse transformation is also possible by erasing all indices
and adding parentheses around subexpressions with nonzero explicit submatch index.
Therefore RE and IRE are equivalent representations.
    \begin{align*}
    &\begin{aligned}
        mark &: \XR_\Sigma \longrightarrow \XIR_\Sigma \\
        mark &(x) \mid_{x \in \{\epsilon, \alpha\}} = (0, 0, x) \\
        %
        mark &(e_1 \circ e_2) \mid_{\circ \in \{|,\cdot\}} = (i, 0,
            (i, j_1, r_1) \circ
            (i, j_2, r_2)
            ) \\
            &\text{where }            (i_1, j_1, r_1) = mark(e_1) \\
            &\space{\hphantom{where }}(i_2, j_2, r_2) = mark(e_2) \\
            &\space{\hphantom{where }}i = i_1 \vee i_2 \\
        %
        mark &(e^{n, m}) \mid_{e = (e_1)} = (1, 0, (1, 1, r)) \\
            &\text{where } (\Xund, \Xund, r) = mark(e_1) \\
        %
        mark &(e^{n, m}) \mid_{e \neq (e_1)} = (i, 0, (i, j, r)) \\
            &\text{where } (i, j, r) = mark(e) \\
        %
        mark &((e)) = mark((e)^{1, 1})
    \end{aligned}
    %
    &&\begin{aligned}
        enum &: \YZ \times \YZ \times \XIR_\Sigma \longrightarrow \YZ \times \YZ \times \XIR_\Sigma \\
        enum &(\bar{i}, \bar{j}, (i, j, x)) \mid_{x \in \{\epsilon, \alpha\}}
            = (\bar{i} + i, \bar{j} + j, (\bar{i} \times i, \bar{j} \times j, x))
        \\
        enum &(\bar{i}, \bar{j}, (i, j, r_1 \circ r_2)) \mid_{\circ \in \{|,\cdot\}}
            = (i_2, j_2, (\bar{i} \times i, \bar{j} \times j, \bar{r}_1 \circ \bar{r}_2)) \\
            &\text{where }            (i_1, j_1, \bar{r}_1) = enum(\bar{i} + i, \bar{j} + j, r_1) \\
            &\space{\hphantom{where }}(i_2, j_2, \bar{r}_2) = enum(i_1, j_1, r_2)
        \\
        enum &(\bar{i}, \bar{j}, (i, j, r^{n,m})) = (i_1, j_1, (\bar{i} \times i, \bar{j} \times j, \bar{r}^{n,m})) \\
            &\text{where }
                (i_1, j_1, \bar{r}) = enum(\bar{i} + i, \bar{j} + j, r)
    \end{aligned}
    \end{align*}

Just like REs denote sets of PTs, IREs denote sets of \emph{IPTs} --- \emph{indexed parse trees}.
The only difference between PTs and IPTs is that each node of an IPT has an associated number ---
the implicit submatch index inherited from the corresponding IRE node (denoted with a superscript).
Explicit submatch index is not used in IPTs.
%
As for PTs, $str(t)$ denotes the string formed by concatenation of all alphabet symbols in the left-to-right traversal of $t$,
and $\IPT(r, w) = \{ t \in \IPT(r) \mid str(t) = w \}$ is the set of all IPTs for an IRE $r$ and a string $w$.
%
Examples of IPTs can be seen on figure \ref{fig_mark_enum}.

    \begin{Xdef}
    \emph{Indexed parse trees (IPT)} over finite alphabet $\Sigma$, denoted $\XIT_\Sigma$, are:
    \begin{enumerate}
        \item Atomic IPTs:
          \emph{nil tree} ${\varnothing}^i \in \XIT_\Sigma$,
          \emph{empty tree} ${\epsilon}^i \in \XIT_\Sigma$ and
          \emph{unit tree} ${\alpha}^i \in \XIT_\Sigma$, where $\alpha \in \Sigma$ and $i \in \YZ$.
        \item Compound IPTs: if $t_1, \dots, t_n \in \XIT_\Sigma$, where $n \geq 1$, and $i \in \YZ$, then
          ${T}^i(t_1, \dots, t_n) \in \XIT_\Sigma$.
    \end{enumerate}
    \end{Xdef}

The operator $\IPT: \XIR_\Sigma \rightarrow 2^{\XIT_\Sigma}$ gives the set of all IPTs denoted by the given IRE:
%(its definition is very similar to the one of operator $PT$):
    \begin{align*}
        \IPT\big((i, \Xund, \epsilon)\big) &= \{ {\epsilon}^{i} \}
        \\
        \IPT\big((i, \Xund, \alpha)\big) &= \{ {\alpha}^{i} \}
        \\
        \IPT\big((i, \Xund, (i_1, j_1, r_1) \mid (i_2, j_2, r_2))\big) &=
            \big\{ {T}^{i}(t, \varnothing^{i_2}) \mid t \in \IPT\big((i_1, j_1, r_1)\big) \big\} \cup
            \big\{ {T}^{i}(\varnothing^{i_1}, t) \mid t \in \IPT\big((i_2, j_2, r_2)\big) \big\}
        \\
        \IPT\big((i, \Xund, (i_1, j_1, r_1) \cdot (i_2, j_2, r_2))\big) &=
            \big\{ {T}^{i}(t_1, t_2) \mid
                t_1 \in \IPT\big((i_1, j_1, r_1)\big),
                t_2 \in \IPT\big((i_2, j_2, r_2)\big)
            \big\} \\
        \IPT\big((i, \Xund, (i_1, j_1, r_1)^{n, m})\big) &=
            \begin{cases}
                \big\{ {T}^{i}(t_1, \dots, t_m) \mid t_k \in \IPT\big((i_1, j_1, r_1)\big) \;
                    \forall k = \overline{1, m} \big\} \cup \{ {T}^{i}(\varnothing^{i_1}) \} &\text{if } n = 0 \\
                \big\{ {T}^{i}(t_n, \dots, t_m) \mid t_k \in \IPT\big((i_1, j_1, r_1)\big) \;
                    \forall k = \overline{n, m} \big\} &\text{if } n > 0
            \end{cases}
    \end{align*}

\emph{Positions} for IPTs are defined in the same way as for PTs, and
$Pos(t)$ denotes the set of all positions of an IPT $t$.
Additionally, we define a set of \emph{submatch positions} as
$Sub(t) = \{ p \mid \exists t|_p = s^i : i \neq 0 \}$.
In other words, $Sub(t)$ is a subset of $Pos(t)$ that contains positions of subtrees with nonzero implicit submatch index.
Intuitively, this is the set of positions that are important for submatch extraction:
in the case of ambiguity we do not need to consider the full trees,
just the relevant parts of them.
%
IPTs have two definitions of norm, one for $Pos$ and one for $Sub$,
which we call \emph{p-norm} and \emph{s-norm} respectively:

\FloatBarrier

    \begin{Xdef}\label{tnorm_of_IPTs}
    The \emph{p-norm} and \emph{s-norm} of an IPT $t$ at position $p$ are:
    \begin{align*}
        \pnorm{t}{p} =
            \begin{cases}
                -1          &\text{if } p \in Pos(t) \text{ and } t|_p = \varnothing^i  \\
                |str(t|_p)| &\text{if } p \in Pos(t) \text{ and } t|_p \neq \varnothing^i \\
                \infty      &\text{if } p \not\in Pos(t)
            \end{cases}
    \quad\quad\quad
        \snorm{t}{p} =
            \begin{cases}
                -1          &\text{if } p \in Sub(t) \text{ and } t|_p = \varnothing^i  \\
                |str(t|_p)| &\text{if } p \in Sub(t) \text{ and } t|_p \neq \varnothing^i \\
                \infty      &\text{if } p \not\in Sub(t)
            \end{cases}
    \end{align*}
    \end{Xdef}

%In other words, the norm is infinite for all positions not in $Sub(t)$,
%and for positions in $Sub(t)$ it depends on the form of subtree:
%for nil subtrees it equals $-1$,
%and for other subtrees it equals the number of symbols.
%We shorten $\|t\|_\Lambda$ as $\|t\|$.

Accordingly, IPTs have two definitions of order:
\emph{p-order} based on p-norm
and \emph{s-order} based on s-norm.

    \begin{Xdef}\label{total_order_on_IPTs}
    \emph{P-order on IPTs.}
    Given parse trees $t, s \in PT(e, w)$, we say that $t <_p s$ w.r.t. \emph{desision position} $p$
    iff $\pnorm{t}{p} > \pnorm{s}{p}$ and $\pnorm{t}{q} = \pnorm{s}{q} \; \forall q < p$.
    We say that $t < s$ iff $t <_p s$ for some $p$.
    \end{Xdef}

    \begin{Xdef}\label{partial_order_on_IPTs}
    \emph{S-order on IPTs.}
    Given parse trees $t, s \in PT(e, w)$, we say that $t \prec_p s$ w.r.t. \emph{desision position} $p$ % $p \in Sub(t) \cup Sub(s)$
    iff $\snorm{t}{p} > \snorm{s}{p}$ and $\snorm{t}{q} = \snorm{s}{q} \; \forall q < p$.
    We say that $t \prec s$ iff $t \prec_p s$ for some $p$.
    \end{Xdef}

P-order is defined in exactly the same way as the order on PTs.
S-order, however, has an important difference: is not total, as
there might be two distinct IPTs that coincide in all submatch positions, yet differ in some non-submatch positions.
For such trees s-order is not defined: none of them is less than the other one,
and therefore they are called \emph{incomparable}.
From submatch extraction perspective, incomparable IPTs are indistinguishable.

    \begin{Xdef}\label{incomparable_IPTs}
    IPTs $t$ and $s$ are \emph{incomparable}, denoted $t \sim s$,
    iff neither $t \prec s$, nor $s \prec t$.
    \end{Xdef}

Incomparability relation is an equivalence relation: it is
reflexive (obviously $s \sim s$),
symmetric (obviously $s \sim t$ implies $t \sim s$) and
transitive (lemma \ref{lemma_ptorder_transitivity_of_incomparability} in appendix shows that $s \sim t \wedge t \sim u$ implies $s \sim u$).
Therefore all IPTs of a given RE can be partitioned into \emph{incomparability classes}.
%
Unlike the case of PTs, where the minimal PT is unique,
in case of IPTs there is a whole class of minimal trees:
$\IPT_{min}(r,w) = \{ t \in \IPT(r,w) \mid \forall u \in \IPT(r,w) : t \sim u \vee t < u \}$.

%as theorem \ref{theorem_porder_on_IPTs} states, p-order is a strict total order.
%As the theorem \ref{theorem_sorder_on_IPTs} states, s-order is a strict weak order.

    \begin{XThe}\label{theorem_porder_on_IPTs}
    P-order $<$ is a strict total order on IPTs.
    \end{XThe}

    \begin{XThe}\label{theorem_sorder_on_IPTs}
    S-order $\prec$ is a strict weak order on IPTs.
    \end{XThe}

\begin{figure}\label{fig_mark_enum}
\includegraphics[width=\linewidth]{img/mark_enum.pdf}
\caption{
An example of constructing IRE for RE $(\epsilon|a^{0,\infty})(a|\epsilon)^{0,3}$ using $mark$ and $enum$\\
and some examples of IPT for the resulting IRE and string ``$a$''.
S-norm of each subtree is marked with $\#$.
}
\end{figure}

What is the relation between the total p-order $<$ and the partial s-order $\prec$ on IPTs?
Can we say that p-order is an extension of s-order on non-comparable IPTs?
We show by the means of a counterexample that the answer to the above question is negative.
Consider the IPTs $t$ and $u$ on figure \ref{fig_mark_enum}.
On one hand, we have $t \prec_{2.2} u$, because $\snorm{t}{2.2} = \infty > 0 = \snorm{u}{2.2}$ and s-norms at all preceding submatch positions agree.
On the other hand, we have $u <_{1.1} t$, because $\pnorm{t}{1.1} = -1 < 0 = \pnorm{u}{1.1}$
and p-norms at all preceding positions agree.
So, p-order is not necessarily an extension of s-order.
%
However, the two orders are ``compatible'' in the following sense:
they agree on the notion of the minimal tree (the exact meaning of this is formalized by theorem \ref{theorem_order_compat}).
%
This is an important result becuse it means that
if we keep refining submatch granularity by tunrning more and more sub-RE into submatch groups,
we will continuously narrow down the class of $\prec$-minimal trees,
until we are left with a unique $<$-minimal tree.
In practice this means that adding a few parentheses in RE will not drastically change the previous results of submatch extraction;
it will only add more details.

    \begin{XThe}\label{theorem_order_compat}
    For an IRE $r$ and string $w$,
    let $t_{min}$ be the $<$-minimal tree in $\IPT(r,w)$
    and let $T_{min} = \IPT_{min}(r,w)$ be the class of the $\prec$-minimal trees in $\IPT(r,w)$.
    Then $t_{min} \in T_{min}$.
    \end{XThe}

In the rest of the paper the words ``order'' and ``norm`` refer to s-order and s-norm.

\FloatBarrier

\section{Parenthesized expressions}

In this section we introduce linearised representation of parse trees: \emph{parenthesized expressions}.
%The structure of the section follows \cite{OS13},
%however there are subtle, but important differences in some of the definitions and proofs.

    \begin{Xdef}
    \emph{Parenthesized expressions (PEs)} over finite alphabet $\Sigma$, denoted $\XP_\Sigma$, are:
    \begin{enumerate}
        \item Atomic PE:
          \emph{nil expression} $\Xm \in \XP_\Sigma$,
          \emph{empty expression} $\epsilon \in \XP_\Sigma$ and
          \emph{unit expression} $a \in \XP_\Sigma$, where $\alpha \in \Sigma$.
        \item Compound PE: if $e_1, e_2 \in \XP_\Sigma$, then
            $e_1 e_2 \in \XP_\Sigma$ and
            $\Xl e_1 \Xr \in \XP_\Sigma$.
    \end{enumerate}
    \end{Xdef}

Parenthesis $\Xl$ is called \emph{opening} and
parenthesis $\Xr$ is called \emph{closing};
the \emph{nil}-parenthesis $\Xm$ is both opening and closing.
The \emph{height} of parenthesis in a PE is the number of preceding opening parentheses (including this one)
minus the number of preceding closing parentheses (including this one).
For convenience we sometimes explicitly denote height with subscript:
this allows us to consider (not necessarily correctly nested) fragments of the given PE in isolation,
without losing the context of the whole PE.
However, height is not a part of parenthesis itself
and is not taken into account when comparing the elements of PEs.
Function $\Phi : \YZ \times \XT_\Sigma \rightarrow \XP_\Sigma$ transforms PTs into PEs:
    $$
    \Phi_{h}(t^{i}) = \begin{cases}
        str(t^{i})                                            &\text{if } i = 0 \\
        \Xm_h                                                 &\text{if } i \neq 0 \wedge t = \varnothing \\
        \Xl_{h+1} \Xr_h                                       &\text{if } i \neq 0 \wedge t = \epsilon \\
        \Xl_{h+1} a \Xr_h                                     &\text{if } i \neq 0 \wedge t = a \in \Sigma \\
        \Xl_{h+1} \Phi_{h+1}(t_1) \dots \Phi_{h+1}(t_n) \Xr_h &\text{if } i \neq 0 \wedge t = T(t_1, \dots, t_n)
    \end{cases}
    $$

For a given RT $r$ and string $w$, the set $\big\{ \Phi_{0}(t) \mid t \in PT(r, w) \big\}$ is denoted $PE(r, w)$.
If $\alpha, \beta \in PE(r, w)$ for some $r$ and $w$, we say that $\alpha$ and $\beta$ are \emph{comparable}.
%
For PE $\alpha$, $\beta$,
$\alpha \sqcap \beta$ denotes the longest common prefix of $\alpha$ and $\beta$,
$\alpha \backslash \beta$ denotes the suffix of $\alpha$ after removing $\alpha \sqcap \beta$,
$lasth(\alpha)$ denotes the height of the last parenthesis in $\alpha$ or $\infty$ if $\alpha$ is empty or begins with a letter,
$minh(\alpha)$ denotes the minimal height of parenthesis in $\alpha$ or $\infty$ if $\alpha$ is empty or begins with a letter,
$first(\alpha)$ denotes the first parenthesis in $\alpha$ or $\bot$ if $\alpha$ is empty or begins with a letter.
Each PE $\alpha$ can be represented as $\alpha_0 a_1 \alpha_1 \dots a_n \alpha_n$,
where $\alpha_i$ is the $i$-th \emph{frame} --- the possibly empty sequence of parentheses between
subsequent alphabet symbols $a_i$ and $a_{i+1}$ or the beginning or end of $\alpha$.
Note that comparable PE have the same number of frames.
For distinct comparable PE $\alpha$, $\beta$
the index of the first distinct pair of frames is called \emph{fork}.

    \begin{Xdef}
    Let $\alpha$, $\beta$ be distinct comparable PE, such that
    $\alpha = \alpha_0 a_1 \alpha_1 \dots a_n \alpha_n$,
    $\beta = \beta_0 a_1 \beta_1 \dots a_n \beta_n$ and $k$ is the fork.
    We define $trace (\alpha, \beta)$ as the sequence $(\rho_0, \dots, \rho_n)$, where:
    $$
    \rho_i = \begin{cases}
        -1 &\text{if } i < k \\
        min (lasth (\alpha_i \sqcap \beta_i), minh(\alpha_i \backslash \beta_i)) &\text{if } i = k \\
        min (\rho_{i-1}, minh(\alpha_i)) &\text{if } i > k
    \end{cases}
    $$
    We write $traces(\alpha, \beta)$ to denote $\big( trace (\alpha, \beta), trace (\beta, \alpha) \big)$.
    \end{Xdef}

\begin{figure}\label{fig_pe}
\includegraphics[width=\linewidth]{img/pe.pdf}
\caption{
Examples: (a) -- (d): four main rules of POSIX comparison,
(e) -- pairwise comparison of PEs.
}
\end{figure}

    \begin{Xdef}\label{prec1}
    Let $\alpha$, $\beta$ be comparable PE and
    $traces(\alpha, \beta) = \big( (\rho_0, \dots, \rho_n), (\rho'_0, \dots, \rho'_n) \big)$.
    The \emph{longest-precedence} relation $\sqsubset$ is defined as
    $\alpha \sqsubset \beta \Leftrightarrow \exists i \leq n:
        \big( \rho_i > \rho'_i \big) \wedge
        \big( \rho_j = \rho'_j \; \forall j > i \big)$.
%    $$
%        \alpha \sqsubset \beta \quad \Leftrightarrow \quad \exists i \leq n:
%        \prescript{}{\wedge}{\left[
%            \begin{aligned}
%                &\rho_i > \rho'_i \\
%                &\forall j > i: \rho_j = \rho'_j
%            \end{aligned}
%        \right.}
%    $$
    If neither $\alpha \sqsubset \beta$, nor $\beta \sqsubset \alpha$,
    then $\alpha$, $\beta$ are \emph{longest-equivalent}: $\alpha \sim \beta$
    (note that in this case $\rho_i = \rho'_i \; \forall i = \overline {1, n}$).
    \end{Xdef}

    \begin{Xdef}\label{prec2}
    Let $\alpha$, $\beta$ be comparable PE, and let
    $x = first (\alpha \backslash \beta)$,
    $y = first (\beta \backslash \alpha)$.
    The \emph{leftmost-precedence} relation $\subset$ is defined as
    $\alpha \subset \beta \Leftrightarrow x < y$, where
    the set of possible values of $x$ and $y$ is ordered as follows:
    $\bot < \Xr < \Xl < \Xm$.
%    Let $\alpha$, $\beta$ be comparable PE, and let
%    $x = first (\alpha \backslash \beta)$,
%    $y = first (\beta \backslash \alpha)$.
%    The \emph{leftmost-precedence} relation $\subset$ is defined as follows:
%    $\alpha \subset \beta \Leftrightarrow
%    \big(x = \bot \wedge y \not= \bot \big) \vee
%    \big(x = \Xr \wedge y \not= \bot \big) \vee
%    \big(x = \Xl \wedge y = \bar{\Xl} \big)$.
%
%    $$
%        \alpha \subset \beta \quad \Leftrightarrow \quad
%        \prescript{}{\vee \;}{\left[
%            \begin{aligned}
%                &x = \bot   &&\wedge && y \not= \bot \\
%                &x = \Xr    &&\wedge && y \not= \bot \\
%                &x = \Xl    &&\wedge && y = \bar{\Xl}
%            \end{aligned}
%        \right.}
%    $$
    \end{Xdef}

    \begin{Xdef}\label{pe_order}
    The \emph{longest-leftmost-precedence} relation $<$ on comparable PE is defined as
    $\alpha < \beta \Leftrightarrow
        \big( \alpha \sqsubset \beta \big) \vee
        \big( \alpha \sim \beta \wedge \alpha \subset \beta \big)$.
%    \begin{align*}
%        \alpha < \beta \quad \Leftrightarrow \quad
%        \prescript{}{\vee}{\left[
%            \begin{aligned}
%                &\alpha \sqsubset \beta \\
%                &\alpha \sim \beta \wedge \alpha \subset \beta
%            \end{aligned}
%        \right.}
%    \end{align*}
    \end{Xdef}

    \begin{XThe}\label{theorem_order_on_pe_same_as_on_pt}
    Let $s, t \in PT(r, w)$, then
    $s <_p t \Leftrightarrow \Phi_{h}(s) < \Phi_{h}(t) \; \forall h$.
    \end{XThe}

\FloatBarrier


\section{Tagged NFA}

    \begin{Xdef}
    \emph{Tagged Nondeterministic Finite Automaton (TNFA)}
    is a structure $(\Sigma, Q, T, \Delta, q_0, q_f)$, where:
    \begin{itemize}
        \item[] $\Sigma$ is a finite set of symbols (\emph{alphabet})
        \item[] $Q$ is a finite set of \emph{states}
        \item[] $T\subset\YN$ is a finite set of \emph{tags}
        \item[] $\Delta = \Delta^\Sigma \sqcup \Delta^\epsilon$ is the \emph{transition} relation, where:
        \begin{itemize}
            \item[] $\Delta^\Sigma \subseteq Q \times \Sigma \times \{\epsilon\} \times Q$ (transitions on symbols)
            \item[] $\Delta^\epsilon \subseteq Q \times \YN \times \big( \YN \cup \{\epsilon\} \big) \times Q$ ($\epsilon$-transitions)
            \item[]
                and all $\epsilon$-transitions from the same state have different priority:
                $\forall (q, n, \Xund, \Xund), (q, m, \Xund, \Xund) \in \Delta^\epsilon: n \neq m$.
        \end{itemize}
        \item[] $q_0 \in Q$ is the \emph{initial} state
        \item[] $q_f \in Q$ is the \emph{final} state
    \end{itemize}
    \end{Xdef}

TNFA construction is given by the $F$ function defined on figure \ref{fig_tnfa}.


\begin{figure*}
\begin{multicols}{2}
\fontsize{8}{10}
    \setstretch{0.8}

    %\fontsize{9.5pt}{11.5pt}\selectfont

    %\newcommand \retonfa {re \Xund to \Xund n\!f\!a}
    %\newcommand \ntag {neg \Xund tag}
    \newcommand \retonfa {F}
    \newcommand \ntag {N}

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{}
    \Fn {$\underline{\retonfa(r, y)} \smallskip$} {
        \If {$r = (0, 0, \epsilon)$} {
            \Return $(\Sigma, \{y\}, \emptyset, \emptyset, y, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, \alpha) \mid_{\alpha \in \Sigma}$} {
            \Return $(\Sigma, \{x,y\}, \emptyset, \{(x, \alpha, \epsilon, y)\}, x, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, s \cdot u)$} {
            $(\Sigma, Q_s, T_s, \Delta_1, x, y) = \retonfa (s, y)$ \;
            $(\Sigma, Q_u, T_u, \Delta_2, z, x) = \retonfa (u, x)$ \;
            \Return $(\Sigma, Q_s \cup Q_u, T_s \cup T_u, \Delta_s \cup \Delta_u, z, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, s \mid u)$} {
            $(\Sigma, Q_1, T_1, \Delta_1, x_1, y) = \ntag (u, y)$ \;
            $(\Sigma, Q_2, T_2, \Delta_2, x_2, x_1) = \retonfa (s, x_1)$ \;
            $(\Sigma, Q_3, T_3, \Delta_3, x_3, y) = \retonfa (u, y)$ \;
            $(\Sigma, Q_4, T_4, \Delta_4, x_4, x_3) = \ntag (s, x_3)$ \;
            $Q = Q_1 \cup Q_2 \cup Q_3 \cup Q_4 \cup \{x\}$ \;
            $T = T_1 \cup T_2 \cup T_3 \cup T_4$ \;
            $\Delta = \Delta_1 \cup \Delta_2 \cup \Delta_3 \cup \Delta_4 \cup \{(x,1,\epsilon,x_2), (x,2,\epsilon,x_4)\}$ \;
            \Return $(\Sigma, Q, T, \Delta, x, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, s^{n,m}) \mid_{n > 0}$} {
            $(\Sigma, Q_1, T_1, \Delta_1, x, y) = \retonfa ((0, 0, s^{n-1,m}), y)$ \;
            $(\Sigma, Q_2, T_2, \Delta_2, z, x) = \retonfa (s, x)$ \;
            \Return $(\Sigma, Q_1 \cup Q_2, T_1 \cup T_2, \Delta_1 \cup \Delta_2, z, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, s^{0,m})$} {
            $(\Sigma, Q_1, T_1, \Delta_1, x_1, y) = \retonfa ((0, 0, s^{1,m}), y)$ \;
            $(\Sigma, Q_2, T_2, \Delta_2, x_2, y) = \ntag (s, y)$ \;
            $Q = Q_1 \cup Q_2 \cup \{x\}$ \;
            $\Delta = \Delta_1 \cup \Delta_2 \cup \{(x,1,\epsilon,x_1), (x,2,\epsilon,x_2)\}$ \;
            \Return $(\Sigma, Q, T_1 \cup T_2, \Delta, x, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, s^{1,\infty})$} {
            $(\Sigma, Q_1, T_1, \Delta_1, z, x) = \retonfa (s, \Xund)$ \;
            $Q = Q_1 \cup \{y\}$ \;
            $\Delta = \Delta_1 \cup \{(x,1,\epsilon,z), (x,2,\epsilon,y)\}$ \;
            \Return $(\Sigma, Q, T_1, \Delta, z, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, s^{1,1})$} {
            \Return $\retonfa (s, y)$
        }
        \BlankLine
        \ElseIf {$r = (0, 0, s^{1,m}) \mid_{1 < m < \infty}$} {
            $(\Sigma, Q_1, T_1, \Delta_1, x, y) = \retonfa ((0, 0, s^{1,m-1}), y)$ \;
            $(\Sigma, Q_2, T_2, \Delta_2, w, z) = \retonfa (r_1, \Xund)$ \;
            $\Delta = \Delta_1 \cup \Delta_2 \cup \{(z,1,\epsilon,y), (z,2,\epsilon,x)\}$ \;
            \Return $(\Sigma, Q_1 \cup Q_2, T_1 \cup T_2, \Delta, w, y)$
        }
        \BlankLine
        \ElseIf {$r = (i, \Xund, s) \mid_{i \neq 0}$} {
            $(\Sigma, Q_1, T_1, \Delta_1, z, x) = \retonfa (s, \Xund)$ \;
            $Q = Q_1 \cup \{w, y\}$ \;
            $T = T_1 \cup \{2i\!-\!1, 2i\}$ \;
            $\Delta = \Delta_1 \cup \{(w,1,2i\!-\!1,z), (x,1,2i,y)\}$ \;
            \Return $(\Sigma, Q, T, \Delta, w, y)$
        }
    }
    \end{algorithm}


    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{}
    \Fn {$\underline{\ntag(r)} \smallskip$} {
        $T = \{ t_1, \dots, t_n \} = T(r), n \geq 0$ \;
        $Q = \{x_0, \dots, x_{2n}\}$ \;
        $\Delta = \{(x_{2i-2},1,1\!-\!2t_i, x_{2i-1}), (x_{2(n-i)-1}, 1, -\!2t_i, x_{2(n - i)})\}_{i=1}^{n}$ \;
        \Return $(\Sigma, Q, T, \Delta, x_0, x_{2n})$ \;
    }
    \end{algorithm}


    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{}
    \Fn {$\underline{T((i, \Xund, r))} \smallskip$} {
        \lIf {$i = 0$} {
            \Return $\emptyset$
        }
        \lElseIf {$r = s \mid u \vee r = s \cdot u$} {
            \Return $\{i\} \cup T(s) \cup T(u)$
        }
        \lElseIf {$r = s^{n,m}$} {
            \Return $\{i\} \cup T(s)$
        }
        \lElse {
            \Return $\{i\}$
        }
    }
    \end{algorithm}


    \columnbreak


    \includegraphics[width=\linewidth]{img/tnfa_construction.pdf}


\end{multicols}
\vspace{-2em}
\caption{TNFA construction.}
\end{figure*}



\begin{figure}\label{fig_tnfa_example}
\includegraphics[width=\linewidth]{img/tnfa_example.pdf}
\vspace{-2em}
\caption{
    Example TNFA for RE $(a|\epsilon)^{0,3}((a^{0,\infty})|(\epsilon))$.
}
\end{figure}


\FloatBarrier


\begin{figure*}
\begin{multicols}{2}
    \setstretch{0.8}
    \newcommand \ff {f\!\!f}

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{match (\XN, \alpha_1 \dots \alpha_n)} \smallskip$} {
        $(\Sigma, Q, F, q_0, T, \Delta) = \XN$ \;
        $P_1, P_2: Q \times Q \rightarrow \YZ$ \;
        \BlankLine

        $X = closure(\{ (\bot, q_0, \epsilon, t_0) \}, F, \Delta, P_1, P_2)$ \;
        $(X, B, D) = step(0, X, P_1, P_2)$ \;

        \BlankLine
        \For {$i = \overline{1,n}$} {
            $X = reach(X, \Delta, \alpha_i)$ \;
            $X = closure(X, Q, F, \Delta, P_1, P_2)$ \;
            $(X, P_1, P_2) = step(i, X, P_1, P_2)$ \;
        }

        \BlankLine
        \If {$\exists (\Xund, p, \Xund, t) \in X \mid p \in F$} {
            \Return $output(t)$
        } \lElse {
            \Return $\bot$
        }
    }
    \end{algorithm}


    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{reach (X, \alpha)} \smallskip$} {
        \Return $\{ (q, p, \epsilon, t \cdot u) \mid $ \\
            $\hspace{4em} (\Xund, q, u, t) \in X \wedge (q, \alpha, \epsilon, p) \in \Delta^\Sigma \}$
    }
    \end{algorithm}


    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{step(k, X, P_1, P_2)} \smallskip$} {
        $\{ x_i \}_{i=1}^{n} = \{(q_i, p_i, u_i, t_i) \}_{i=1}^{n} = X$ \;

        \For {$i = \overline {1, n}$} {
            \For {$j = \overline {1, n}$} {
                $(h_1, h_2, l) = precedence (x_i, x_j, P_1, P_2)$ \;
                $P_1' [p_i] [p_j] = h_1, \; P_2' [p_i] [p_j] = l$ \;
                $P_1' [p_j] [p_i] = h_2, \; P_2' [p_j] [p_i] = -l$
            }
        }
        \BlankLine
        \Return $(X, P_1', P_2')$ \;
    }
    \end{algorithm}

    \columnbreak

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline {precedence (x, y, P_1, P_2)} \smallskip$} {
        $(q, \Xund, \gamma, \Xund) = x$, where $\gamma = a_1 \dots a_n, \; n \geq 0$ \;
        $(p, \Xund, \delta, \Xund) = y$, where $\delta = b_1 \dots b_m, \; m \geq 0$ \;
        $k = 1, \; hx = hy = \infty$ \;
        $\ff = (q = p)$ \tcp{is fork frame?}

        \BlankLine
        \tcp{identical}
        \lIf { $\ff \wedge \gamma = \delta$ } {
            \Return $(hx, hy, 0)$
        }

        \BlankLine
        \tcp {longest-precedence}
        \If { $\ff$ } {
            \lWhile {$k \leq min (n, m) \wedge a_k = b_k$} {
              $k = k + 1$ %\tcp{first mismatch}
            }
            \lIf {$k > 1$} {
                $hx = hy = height (a_{k-1})$
            }
        } \Else {
            $hx = P_1 [q] [p], \; hy = P_1 [p] [q]$
        }
        \lFor {$i = \overline{k, n}$} {
            $hx = min (hx, height (a_i))$
        }
        \lFor {$i = \overline{k, m}$} {
            $hy = min (hy, height (b_i))$
        }
        \lIf {$hx > hy$} {\Return $(hx, hy, -1)$}
        \lIf {$hx < hy$} {\Return $(hx, hy, 1)$}

        \BlankLine
        \tcp {leftmost-precedence}
        \If { $\ff$ } {
            \lIf {$k = n = m$} { $l = 0$ }
            \lElseIf {$k = n$} { $l = -1$ }
            \lElseIf {$k = m$} { $l = 1$ }
            \lElseIf {$a_k mod 2 \equiv 0$} { $l = -1$ }
            \lElseIf {$b_k mod 2 \equiv 0$} { $l = 1$ }
            \lElseIf {$a_k > b_k$} { $l = -1$ }
            \lElseIf {$a_k < b_k$} { $l = 1$ }
        } \lElse {
            $l = P_2 [q] [p]$
        }
        \Return $(hx, hy, l)$
    }
    \end{algorithm}
\end{multicols}
\vspace{-2em}
\begin{center}
\caption{Matching algorithm.}
\end{center}
\end{figure*}


\begin{figure*}
\begin{multicols}{2}
    \setstretch{0.8}
    \newcommand \outputoffsets {out\!put \Xund o\!f\!\!f\!sets}
    \newcommand \outputparsetree {out\!put \Xund parse \Xund tree}
    \newcommand \parsetree {parse \Xund tree}

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{}
    \Fn {$\underline{\outputparsetree(s)} \smallskip$} {
        \Return $\parsetree(s,1)$
    }
    \end{algorithm}

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{}
    \Fn {$\underline{\parsetree(s, i)} \smallskip$} {
        \lIf {$s = \epsilon$} {
            \Return $\epsilon^i$
        }
        \lIf {$s = \alpha \in \Sigma$} {
            \Return $\alpha^i$
        }
        $a_0 \dots a_n = s$ where $n \geq 1$ \;
        $j = k = 0$ \;
        \While {$k < n$} {
            $k' = k$ \;
            $i' = (|a_{k'}| + 1) / 2$ \;
            \lWhile {$|a_{k+1}| \geq 2i'$} {
                $k = k + 1$
            }
            $j = j + 1$ \;
            \lIf {$a_{k'} < 0$} {$t_j = \varnothing^{i'}$}
            \lElse {$t_j = \parsetree (a_{k'+1} \dots a_{k-1}, i')$ }
        }
        \Return $T^i(t_1, \dots, t_j)$
    }
    \end{algorithm}

    \columnbreak

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{}
    \Fn {$\underline{\outputoffsets(s)} \smallskip$} {
        $a_1 \dots a_n = s$ \;
        $pos = 0$ \;
        \For {$i = \overline {1, n}$} {
            \lIf {$a_i \in \Sigma$} {
                $pos = pos + 1$
            }
            \Else {
                $p = pos$ \;
                \lIf {$a_i < 0$} {$p = -1$}
                \lIf {$a_i mod 2 \equiv 0$} {$pmatch[|a_i|/2].rm \Xund so = p$}
                \lElse {$pmatch[(|a_i| - 1)/2].rm \Xund eo = p$}
            }
        }
        \Return $pmatch$ \;
    }
    \end{algorithm}
\end{multicols}
\vspace{-2em}
\begin{center}
\caption{Two possible $output()$ functions.}
\end{center}
\end{figure*}



\clearpage
\pagebreak


\begin{figure*}
\begin{multicols}{2}

    \newcommand \NOPASS {O\!F\!F}
    \newcommand \TOPSORT {T\!O\!P}
    \newcommand \LINEAR {L\!I\!N}
    \newcommand \INQUEUE {I\!N}
    \newcommand \OFFQUEUE {OUT}
    \newcommand \Xfalse {f\!al\!se}

    \setstretch{0.85}

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{closure \Xund gor1(X, Q, F, \Delta, P_1, P_2)} \smallskip$} {

        \Indm
        context: $C = (\; Q, F, \Delta, P_1, P_2$ \;
        \Indp
        $,\, topsort, linear : \text{stacks of states } q \in Q$ \;
        $,\, result  : Q \rightarrow \YC^Q \cup \{ \bot \}$ \;
        $,\, status  : Q \rightarrow \{ \NOPASS, \TOPSORT, \LINEAR \}$ \;
        $,\, indeg   : Q \rightarrow \YZ$                          \tcp{in-degree of state}
        $,\, active  : Q \rightarrow \YB$                          \tcp{true if state needs rescan}
        $,\, arcs    : Q \rightarrow 2^\Delta$                     \tcp{ordered set of outgoing transitions}
        $,\, next    : Q \rightarrow \YZ)$                         \tcp{index of current transition}
        \Indm
        \Indp

        \BlankLine
        \For {$q \in Q$} {
            $result(q) = \bot$ \;
            $status(q) = \NOPASS$ \;
%            $indeg(q)  = $ in-degree of $q$ in $\Delta$ \;
            $active(q) = \Xfalse$ \;
%            $arcs(q)   = \{ (q, \epsilon, \Xund, \Xund) \in \Delta \}$ \;
            $next(q)   = 1$ \;
        }

        \BlankLine
        \For {$x = (\Xund, q, \Xund, \Xund) \in X$ in inverse order of $precede_0$} {
            $result(q) = x$ \;
            $push(topsort, q)$
        }

        \BlankLine
        \While {$topsort$ is not empty} {

            \BlankLine
            \While {$topsort$ is not empty} {
                $q = pop(topsort)$ \;

                \If {$status(q) \neq \LINEAR$} {
                    $status(q) = \TOPSORT$ \;

                    \While {$true$} {
                        $p = next \Xund admissible \Xund arc(q, C)$ \;
                        \If {$p = \bot$} {
                            $status(q) = \LINEAR$ \;
                            $push(linear, q)$ \;
                            $break$
                        }
                        \ElseIf {$status(p) = \NOPASS$} {
                            $push(topsort, q)$ \;
                            $push(topsort, p)$ \;
                            $next(p) = 1$ \;
                            $break$
                        }
                        \lElse {$active(p) = true$}
                    }
                }
            }

            \BlankLine
            \While {$linear$ is not empty} {
                $q = pop(linear)$ \;

                \If {$active(q)$} {
                    $next(q) = 1$ \;
                    \While {$true$} {
                        $p = next \Xund admissible \Xund arc(q, C)$ \;
                        \lIf {$p = \bot$} {$break$}
                        \ElseIf {$status(p) = \NOPASS$} {
                            $push(topsort, p)$ \;
                            $next(p) = 1$ \;
                        }
                        \ElseIf {$status(p) = \LINEAR$} {
                            $active(p) = true$ \;
                        }
                    }
                }

                $status(q) = \NOPASS$ \;
                $active(q) = \Xfalse$ \;
            }
        }

%TRIE!!!!!!!
        \BlankLine
        \Return $\big\{ (\Xund, q, \Xund, \Xund) = result(q) \mid core(q, C) \}$
    }
    \end{algorithm}

    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{core (q, C)} \smallskip$} {
        \tcp{is final or has outgoing transitions on symbols}
        \Return $q \in F \vee \exists (q, \alpha, \Xund, \Xund) \in \Delta^\Sigma$ \;
    }
    \end{algorithm}


    \columnbreak


    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{closure \Xund gtop(X, Q, F, \Delta, P_1, P_2)} \smallskip$} {

        \Indm
        context: $C = (\; Q, F, \Delta, P_1, P_2$ \;
        \Indp
        $,\, queue : \text{priority queue of states } q \in Q$ \;
        $,\, result  : Q \rightarrow \YC^Q \cup \{ \bot \}$ \;
        $,\, status  : Q \rightarrow \{ \INQUEUE, \OFFQUEUE\}$     \;
        $,\, indeg   : Q \rightarrow \YZ$                          \tcp{in-degree of state}
        $,\, topord  : Q \rightarrow \YZ$                          \tcp{topological index of state}
        $,\, arcs    : Q \rightarrow 2^\Delta$                     \tcp{ordered set of outgoing transitions}
        $,\, next    : Q \rightarrow \YZ)$                         \tcp{index of current transition}
        \Indm
        \Indp

        \BlankLine
        \For {$q \in Q$} {
            $result(q) = \bot$ \;
            $status(q) = \OFFQUEUE$ \;
%            $indeg(q)  = $ in-degree of $q$ in $\Delta$ \;
%            $topord(q) = \text{ topological index of } q \text { in TNFA}$ \;
%            $arcs(q)   = \{ (q, \epsilon, \Xund, \Xund) \in \Delta \}$ \;
            $next(q)   = 1$ \;
        }

        \BlankLine
        \For {$x = (\Xund, q, \Xund, \Xund) \in X$} {
            $y = result(q)$ \;
            \If {$y = \bot \vee precede(x, y, C)$} {
                $result(q) = x$ \;
                \If {$status(q) \neq \INQUEUE$} {
                    $insert \Xund with \Xund priority(queue, q, topord(q))$ \;
                    $status(q) = \INQUEUE$ \;
                }
            }
        }

        \BlankLine
        \While {$queue$ is not empty} {

            $q = extract \Xund min(queue)$ \;
            $status(q) = \OFFQUEUE$ \;
            $next(q) = 1$ \;

            \While {$true$} {
                $p = next \Xund admissible \Xund arc(q, C)$ \;
                \lIf {$p = \bot$} {$break$}
                \ElseIf {$status(p) \neq \INQUEUE$} {
                    $insert \Xund with \Xund priority(queue, p, topord(p))$ \;
                    $status(p) = \INQUEUE$ \;
                }
            }
        }

%TRIE!!!!!!!
        \BlankLine
        \Return $\big\{ (\Xund, q, \Xund, \Xund) = result(q) \mid core(q, C) \}$
    }
    \end{algorithm}



    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{next \Xund admissible \Xund arc (q, C)} \smallskip$} {
        $\{ a_1, \dots, a_n \} = arcs (q)$ \;
        $i = next (q)$ \;

        \While {$i < n$} {

            $(q, \epsilon, \tau, p) = a_i$ \;
            $next(q) = i = i + 1$ \;
            $x = (o, u \tau, t)$, where $(o, u, t) = result(q)$ \;
            $y = result(p)$ \;

            \If {$y = \bot
                \vee indeg(p) < 2
                \vee precede(x, y, C)$} {
                $result(p) = x$ \;
                \Return $p$
            }
        }

        \Return $\bot$
    }
    \end{algorithm}


    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{precede (x, y, C)} \smallskip$} {
        $(\Xund, \Xund, l) = precedence (x, y, P_1, P_2)$ \;
        \Return $l = -1$ %\tcp{true if x precedes y}
    }
    \end{algorithm}


    \begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip}
    \Fn {$\underline{precede_0 (x, y, C)} \smallskip$} {
        $(p,\Xund,\Xund,\Xund) = x, \; (q,\Xund,\Xund,\Xund) = y$ \;
        \Return $P_2[p][q] < 0$ \;
    }
    \end{algorithm}
\end{multicols}
\vspace{-2em}
\begin{center}
\caption{GOR1 and GTOP closure algorithms.
The definitions of $push$, $pop$, $insert \Xund with \Xund priority$, $extract \Xund min$ \\
$arcs$, $indeg$ and $topord$ are omitted for brevity.
%topological sorting of TNFA states is also left for the reader.
$\YC^Q = Q \times Q \times \YZ^* \times \YZ^*$ is the set of all configurations over $Q$.}
\end{center}
\end{figure*}


\clearpage
\pagebreak

\section{GOR1 correcness proof}

For a given RT $r$,
we say that PE $\alpha$ is \emph{minimal} if $\alpha = PE(t)$ for some minimal $t \in PT(r)$,
and we say that path $\pi$ in TNFA $F(r)$ is \emph{minimal} if $\pi$ induces a minimal PE.

GOR1 correctness proof consists of two parts.
First, we get rid of $\epsilon$-loops by showing that,
on one hand, minmal paths do not contain $\epsilon$-loops,
and on the other hand, GOR1 cancels all paths which contain $\epsilon$-loops.
Second, for paths without $\epsilon$-loops we show right distributivity of path comparison over path concatenation.
The proofs make use of the TNFA nested structure
and the fact that each sub-TNFA is has a unique entry and exit states.
TNFA construct for all possible types of RT are shown on the fugure below.



\begin{figure}\label{fig_gor1}
\includegraphics[width=\linewidth]{img/gor1.pdf}
\caption{
Sub-TNFA for individual sub-RT with submatch groups: \\
(a) -- union, (b) -- product, (c), (d) -- bounded repetition, (e), (f) -- unbounded repetition.
}
\end{figure}

    \begin{XLem}\label{gor1_path_containment}
    Let $r$ be a RE, $\pi = q_1 \overset {\alpha} {\rightsquigarrow} q_2$ a tagged path in TNFA $F(r)$,
    where $\alpha \neq \epsilon$,
    and $h = minh (\alpha)$ the minimal tag height on path $\pi$.
    The following statements are true:
    \begin{enumerate}
        \item There is a position $p$ of length $|p| = h$
            such that $\pi$ fully lies inside of subautomaton $F(r|_p)$.

        \item There no position $p$ of length $|p| > h$
            such that $\pi$ fully lies inside of subautomaton $F(r|_p)$.
    \end{enumerate}
    Proof.
    Obvious from TNFA construction.
    $\square$
    \end{XLem}




    \begin{XLem}\label{gor1_minpaths}
    Minimal paths do not contain tagged $\epsilon$-loops.
    \\
    Proof.

    Suppose, on the contrary, that $\pi$ is a minimal path in TNFA $F(r)$, and that $\pi$ contains at least one $\epsilon$-loop.
    Consider the \emph{last} $\epsilon$-loop in $\pi$:
    it can only come from sub-TNFA of the form $F\big( (i, \Xund, (i_1, \Xund, r_1)^{n,\infty}) \big)$ where $n \geq 0$,
    as this is the only looping TNFA construct.
    Let $w_n$ be the final state of sub-TNFA $F\big( (i_1, \Xund, r_1) \big)$
    as shown on figure \ref{fig_gor1} (e) -- (f).
    Then $\pi$ can be represented as
    $\pi = \pi_1 \pi_2 \pi_3$, where $\pi_2$ is the $\epsilon$-loop:
    $\pi_1 = q_0 \overset {u | \alpha} {\rightsquigarrow} w_n$ and
    $\pi_2 = w_n \overset {\epsilon | \beta} {\rightsquigarrow} w_n$ and
    $\pi_3 = w_n \overset {v | \gamma} {\rightsquigarrow} q_f$.
    Consider path $\pi' = \pi_1 \pi_3$ that is obtained from $\pi$ by removing $\pi_2$.
    It consumes the same input string $uv$ as $\pi$,
    therefore PE transduced by $\pi$ and $\pi'$ are comparable: $\alpha \beta \gamma, \alpha \gamma \in PE(r, uv)$.
    Let $j$ be the total number of repetitions through $F\big( (i_1, \Xund, r_1) \big)$,
    and let $i$ be the index of the $\epsilon$-loop repetition.

    First case: $i = j$.
    In this case fork of $\alpha \beta \gamma$ and $\alpha \gamma$ happens immediately after $(i-1)$-th repetition:
    %
    \begin{alignat*}{10}
        \alpha \beta \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \;&&\big|\; \Xl_h x_{i} \Xr_h \;&&\; \Xr_{h-1} x_{j+1} \\[-0.5em]
        \alpha \gamma       &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \;&&\big|\;                   \;&&\; \Xr_{h-1} x_{j+1}
    \end{alignat*}
    %
    It must be $\alpha \beta \gamma \sim \alpha \gamma$,
    because $minh (\beta) = h > h - 1 = minh (first (\gamma))$,
    so at the fork frame $k$ we have $\rho_k = \rho'_k \leq h - 1$.
    %
    Furthermore, it must be $\alpha \gamma \subset \alpha \beta \gamma$,
    because $first (\gamma) = \Xr < \Xl = first (\beta)$.

    Second case: $i < j$.
    In this case $(i + 1)$-th repetition cannot be an $\epsilon$-loop
    (because we assumed that $i$-th repetition is the \emph{last} $\epsilon$-loop),
    therefore
    fork of $\alpha \beta \gamma$ and $\alpha \gamma$ happens
    inside of $i$-th repetition of $\alpha \beta \gamma$
    and $(i + 1)$-th repetition of $\alpha \gamma$:
    %
    \begin{alignat*}{10}
        \alpha \beta \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \Xl_h y_1 \;&&\big|\; y_2 \Xr_h \Xl_h x_{i+1} \Xr_h && \Xl_h x_{i+2} \Xr_h \hdots \Xl_h x_j \Xr_h \;&&\; \Xr_{h-1} x_{j+1} \\[-0.5em]
        \alpha \gamma       &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \Xl_h y_1 \;&&\big|\; y_3 \Xr_h                     && \Xl_h x_{i+2} \Xr_h \hdots \Xl_h x_j \Xr_h \;&&\; \Xr_{h-1} x_{j+1}
    \end{alignat*}
    %
    In this case
    fork frame of $\alpha \beta \gamma$ contains $y_2 \Xr_h \Xl_h$ fragment, because $y_2$ is part of the $\epsilon$-loop.
    But the fork frame of $\alpha \gamma$ ends inside of $y_3$, because $(i+1)$-th repetiton is not an $\epsilon$-loop and must contain alphabet symbols.
    Therefore at the fork frame $k$ we have $\rho_k = h$ and $\rho'_k > h$.
    All subsequent frames $l > k$ are identical,
    so either $\rho_l = \rho'_l = h'$ (if $l$-th frame contains parentheses of height $h' \leq h$),
    or else $\rho_l = \rho_k$ and $\rho'_l = \rho'_k$.
    Consequently $\alpha \gamma \sqsubset \alpha \beta \gamma$.

    In both cases $\alpha \gamma < \alpha \beta \gamma$,
    which contradicts the fact that $\pi$ is a minimal path.
    $\square$
    \end{XLem}



    \begin{XLem}\label{gor1_loops}
    GOR1 discards paths with tagged $\epsilon$-loops.
    \\
    Proof.

    GOR1 finds non-looping paths before their looping counterparts,
    as it uses depth-first search to explore new paths and prunes ambiguous paths
    immediately after exploring transitions to the join state.
    So for each TNFA state, the first path to be found is a path without $\epsilon$-loops.
    We will show that once GOR1 has found a path without $\epsilon$-loops,
    it will never prefer a path with an $\epsilon$-loop
    (though of course it might prefer some other path without $\epsilon$-loops).

    The only TNFA construct that has a loop is unbounded repetition
    $F\big( (i, \Xund, (i_1, \Xund, r_1)^{n,\infty}) \big)$ where $n \geq 0$,
    shown on figure \ref{fig_gor1} (e) -- (f).
    Consider arbitrary path $\pi$ that contains
    $\epsilon$-loop through sub-TNFA $F\big( (i_1, \Xund, r_1) \big)$.
    %
    Let $q_1$ be the first state on $\pi$ that belongs to the $\epsilon$-loop.
    %
    Path $\pi$ can be represented as $\pi = \pi_1 \pi_2 \pi_3$, where
    $\pi_1 = q_0 \overset {u | \alpha} {\rightsquigarrow} q_1$ and
    $\pi_2 = q_1 \overset {\epsilon | \beta} {\rightsquigarrow} q_1$ and
    $\pi_3 = q_1 \overset {v | \gamma} {\rightsquigarrow} q_f$.
    %
    By the time GOR1 finds path $\pi_1 \pi_2$,
    it must have already found some other path $\pi'_1 = q_0 \overset {u | \alpha'} {\rightsquigarrow} q_1$ without $\epsilon$-loops.
    There are two possible cases: either $\alpha' = \alpha$, or $\alpha' < \alpha$.
    We will show that in both cases $\alpha' < \alpha \gamma$
    and consequently, GOR1 prefers the path without the $\epsilon$-loop.
    Let $k$ be the index of the last frame
    and $\big( (\rho_1, \hdots, \rho_k), (\rho'_1, \hdots, \rho'_k) \big) = traces (\alpha', \alpha \gamma)$.

    First case: $\alpha' = \alpha$.
    Because $\alpha$ is a proper prefix of $\alpha \gamma$,
    fork happens at the last frame and we have
    $\rho_k = lasth(\alpha)$ and
    $\rho'_k = min (lasth(\alpha), minh(\gamma))$.
    If $lasth(\alpha) > minh(\gamma)$, then $\rho_k > \rho'_k$ and $\alpha \sqsubset \alpha \gamma$.
    Otherwise $\rho_k = \rho'_k$ and $\alpha \sim \alpha \gamma$,
    and we have $first(\alpha \backslash \alpha \gamma) = \bot$ and $first(\alpha \gamma \backslash \alpha) \neq \bot$,
    therefore $\alpha \subset \alpha \gamma$.
    In both cases $\alpha < \alpha \gamma$.

    Second case: $\alpha' < \alpha$.
    Let $\big( (\sigma_1, \hdots, \sigma_k), (\sigma'_1, \hdots, \sigma'_k) \big) = traces (\alpha', \alpha)$.
    We have $\rho_k = \sigma_k$ and $\rho'_k = min (\sigma'_k, minh(\gamma)) \leq \sigma_k$.
    If $minh(\gamma) < \sigma'_k$ then $\rho_k > \rho'_k$ and $\alpha' \sqsubset \alpha \gamma$.
    Otherwise $\rho'_k = \sigma'_k$.
    If $\alpha' \sqsubset \alpha$ then $\alpha' \sqsubset \alpha \gamma$.
    Otherwise $\alpha' \sim \alpha$ and $\alpha' \subset \alpha$.
    None of $\alpha$ and $\alpha'$ is a proper prefix of the other,
    because otherwise the longer path has an $\epsilon$-loop through $q_1$, which contradicts our assumption about $\pi_1$ and $\pi'_1$.
    Therefore $first (\alpha' \backslash \alpha) = first (\alpha' \backslash \alpha \gamma)$
    and $first (\alpha \backslash \alpha') = first (\alpha \gamma \backslash \alpha')$.
    Consequently $\alpha' \subset \alpha \implies \alpha' \subset \alpha \gamma$.
    Thus $\alpha' < \alpha \gamma$.
    $\square$
    \end{XLem}





    \begin{XLem} \emph{(Right distributivity of path comparison over path concatenation for $\epsilon$-loop free paths.)}
    Let
    $\pi_\alpha = q_0 \overset {u | \alpha} {\rightsquigarrow} q_1$ and
    $\pi_\beta  = q_0 \overset {u | \beta}  {\rightsquigarrow} q_1$
    be ambiguous paths in TNFA $F(r)$
    and $\pi_\gamma = q_1 \overset {\epsilon | \gamma} {\rightsquigarrow} q_2$
    their common $\epsilon$-suffix,
    such that paths $\pi_\alpha$, $\pi_\beta$
    and the extended paths $\pi_\alpha \pi_\gamma$, $\pi_\beta \pi_\gamma$
    are all free from $\epsilon$-loops.
    Then $\alpha < \beta \implies \alpha \gamma < \beta \gamma$.
    \\
    Proof.

    Let $k = |u|$ be the number of frames in $\alpha$ and $\beta$.
    Let
    $\big( (\rho_1, \hdots, \rho_k),$ $(\rho'_1, \hdots, \rho'_k) \big) = traces (\alpha, \beta)$ and
    $\big( (\sigma_1, \hdots, \sigma_k),$ $(\sigma'_1, \hdots, \sigma'_k) \big) = traces (\alpha \gamma, \beta \gamma)$.
    Obviously for frames $i < k$ we have $\rho_i = \sigma_i$ and $\rho'_i = \sigma'_i$,
    and for the last frame $k$ we have
    $\sigma_k = min (\rho_k, minh (\gamma))$ and
    $\sigma'_k = min (\rho'_k, minh (\gamma))$.
    Consider two possible cases.

    First case: $\alpha \sim \beta \wedge \alpha \subset \beta$.
    %
    We show that $\alpha \gamma \sim \beta \gamma \wedge \alpha \gamma \subset \beta \gamma$.
    %
    We have $\rho_i = \rho'_i \; \forall i$, therefore
    $\sigma_i = \sigma'_i \; \forall i$ and consequently $\alpha \gamma \sim \beta \gamma$.
    Let
    $x = first (\alpha \backslash \beta)$,
    $y = first (\beta \backslash \alpha)$,
    $x' = first (\alpha \backslash \beta \gamma)$ and
    $y' = first (\beta \backslash \alpha \gamma)$.
    None of $\pi_\alpha$ and $\pi_\beta$ is a proper prefix of another,
    otherwise the longer path must contain $\epsilon$-loop through $q_1$
    (because $\alpha$ and $\beta$ have the same number of frames).
    Consequently $x = x'$ and $y = y'$, and we have
    $\alpha \subset \beta$
    $\implies$
    $x < y$
    $\implies$
    $x' < y'$
    $\implies$
    $\alpha \gamma \subset \beta \gamma$.

    Second case: $\alpha \sqsubset \beta$.
    We show that $\alpha \gamma \sqsubset \beta \gamma$.
    %
    If $\rho_k = \rho'_k$ then $\sigma_k = \sigma'_k$
    and obviously $\alpha \gamma \sqsubset \beta \gamma$.
    Else it must be $\rho_k > \rho'_k$.
    In this case, if $minh (\gamma) > \rho'_k$, then $\sigma_k > \sigma'_k$ and again $\alpha \gamma \sqsubset \beta \gamma$.
    Else $minh (\gamma) \leq \rho'_k$ and $\sigma_k = \sigma'_k$.
    In this case, if $k > 1$ and $\rho_{k-1} > \rho'_{k-1}$ then again $\alpha \gamma \sqsubset \beta \gamma$.
    %
    In other words, the only possible case when $\gamma$ can change comparison result is
    when at the last frame we have $\rho_k > \rho'_k$,
    the appended suffix $\gamma$ contains parentheses with low height $minh (\gamma) \leq \rho'_k$
    (so that $\sigma_k = \sigma'_k$),
    and the previous frame doesn't exist
    or compares differently from the last frame: $k = 1$ or $\rho_{k-1} \leq \rho'_{k-1}$.
    We show that in this case the extended path $\pi_\beta \pi_\gamma$ must contain $\epsilon$-loop,
    which contradicts to the lemma condiitons.

    Consider the fragments of paths $\pi_\alpha$ and $\pi_\beta$ from fork to join,
    including (if it exists) the $\epsilon$-transition to the fork state:
    $\pi_\alpha' = q_2 \overset {u | \alpha'} {\rightsquigarrow} q_1$ and
    $\pi_\beta' = q_2 \overset {u | \beta'} {\rightsquigarrow} q_1$.
    We know that $minh (\alpha') = \rho_k$.
%    (because $\rho_k$ is set to the minimal parenthesis height on the path from fork to join).
    Therefore by lemma \ref{gor1_path_containment}
    we know that $\pi_\alpha'$ is contained in a subautomaton $f$ of height $\rho_k$.
    Likewise we know that $\pi_\beta'$ is not contained in $f$, because $minh (\beta') = \rho'_k < \rho_k$.
    %
    Let $\pi_\beta''$ be the part of $\pi_\beta'$ containing the last $k$-th frame,
    and note the following:
    \begin{enumerate}
        \item[(a)] the start state of $\pi_\beta''$ must be contained in $f$
            (because by our assumption
            either $k = 1$ and then start state of $\pi_\beta''$ is the fork state,
            or $\rho_{k-1} \leq \rho'_{k-1}$ which implies $\rho'_{k-1} \geq \rho_k$
            and then all but the last frames of $\pi_\beta'$ must be contained in $f$)
        \item[(b)] $\pi$ cannot be contained in $f$
            (because by our assumption $\rho_k > \rho'_k$)
        \item[(c)] the end state of $\pi_\beta''$ is contained in $f$
            (because it's the join state $q_1$ of $\pi_\alpha'$ and $\pi_\beta'$)
        \item[(d)] $\pi_\gamma$ is not contained in $f$
            (because by our assumption $minh (\gamma) \leq \rho'_k$ and consequently $minh (\gamma) < \rho_k$)
    \end{enumerate}
    %
    Put together, items (a) - (d) mean that the $\epsilon$-path $\pi_\beta'' \pi_\gamma$
    first leaves subautomaton $f$, then re-enters $f$, and then leaves $f$ second time.
    Because $f$ has a unique exit state, this means that $\pi_\beta'' \pi_\gamma$ contains $\epsilon$-loop
    through the exit state of $f$, which contradicts lemma conditions.
    (Effectively it means that $\pi_\beta \pi_\gamma$ is non-minimal and would be discarded by GOR1 anyway.)
%   Note that $\pi_\beta'$ itself does not necessarily contain $\epsilon$-loop.
    %
    $\square$
    \end{XLem}




\section{Matching algorithm}

The final algorithm, complexity estimates.

\section{Conclusions}

\FloatBarrier
\pagebreak

\section*{Appendix}

\subsection*{Proof of Theorem \ref{theorem_order_on_IPTs}}

    \begin{XLem}\label{lemma_ptorder_antisymmetry}
    The order on IPTs is antisymmetric: if $t < s$, then $s \not< t$.
    \\
    Proof.

    Suppose, on the contrary, that $t <_p s$ and $s <_q t$ for some $p$, $q$.
    Without loss of generality let $p \leq q$.
    On one hand $t <_p s$ implies $\|t\|_p > \|s\|_p$.
    On the other hand $s <_q t$ implies $\|t\|_p \leq \|s\|_p$.
    Contradicting the assumption.
    $\square$
    \end{XLem}

    \begin{XLem}\label{lemma_ptorder_transitivity}
    The order on IPTs is transitive: if $t < s$ and $s < u$, then $t < u$.
    \\
    Proof.

    Let $t <_p s$ and $s <_q u$ for some positions $p$, $q$, and let $r = min (p, q)$.
    \\[-1em]

    First, we show that $\|t\|_r > \|u\|_r$.
    If $p \leq q$, we have $\|t\|_p > \|s\|_p$ (implied by $t <_p s$)
    and $\|s\|_p \geq \|u\|_p$ (implied by conjunction $s <_q u \wedge p \leq q$),
    therefore $\|t\|_p > \|u\|_p$.
    Otherwise $p > q$, we have $\|s\|_q > \|u\|_q$ (implied by $s <_q u$)
    and $\|t\|_q = \|s\|_q$ (implied by conjunction $t <_p s \wedge q < p$),
    therefore $\|t\|_q > \|u\|_q$.
    \\[-1em]

    Second, we show that $\forall r' < r$ it holds that $\|t\|_{r'} = \|u\|_{r'}$.
    We have $\|t\|_{r'} = \|s\|_{r'}$ (implied by conjunction $t <_p s \wedge r' < p$)
    and $\|s\|_{r'} = \|u\|_{r'}$ (implied by conjunction $s <_q u \wedge r' < q$),
    therefore $\|t\|_{r'} = \|u\|_{r'}$.
    $\square$
    \end{XLem}

    \begin{XLem}\label{incomparability_equivdef}
    $t \sim s \Leftrightarrow \; \forall p : \|t\|_p = \|s\|_p$.
    \\
    Proof.

    $\Rightarrow$. %First, we show $t \sim s \Rightarrow \forall p : \|t\|_p = \|s\|_p$.
    Suppose, on the contrary, that $\exists p = min \{ q \mid \|t\|_q \neq \|s\|_q \}$,
    then either $t <_p s$ (if $\|t\|_p > \|s\|_p$), or $s <_p t$ (if $\|t\|_p < \|s\|_p$).
    Both cases contradict $t \sim s$.
    \\[-1em]

    $\Leftarrow$.
    $\forall p : \|t\|_p = \|s\|_p$ implies
    $\nexists p : t <_p s$ and $\nexists q : s <_q t$,
    which implies $t \sim s$.
    $\square$
    \end{XLem}

    \begin{XLem}\label{lemma_ptorder_transitivity_of_incomparability}
    Incomparability relation on parse trees is transitive: if $t \sim s$ and $s \sim u$, then $t \sim u$.
    \\
    Proof.

    By lemma \ref{incomparability_equivdef} we have
    $t \sim s \Rightarrow \forall p : \|t\|_p = \|s\|_p$ and
    $s \sim u \Rightarrow \forall p : \|s\|_p = \|u\|_p$,
    therefore by lemma \ref{incomparability_equivdef} $\forall p : \|t\|_p = \|u\|_p \Rightarrow t \sim u$.
    $\square$
    \end{XLem}

The proof of theorem \ref{theorem_order_on_IPTs}
follows from
the lemma \ref{lemma_ptorder_antisymmetry},
the lemma \ref{lemma_ptorder_transitivity} and
the lemma \ref{lemma_ptorder_transitivity_of_incomparability}.


\subsection*{Proof of Theorem \ref{theorem_order_compat}}

First, we prove an auxilary lemma \ref{lemma_subtrees} which
shows that comparison of sub-IPT is justified
if the s-norms at all preceding submatch positions are equal.

    \begin{XLem}\label{lemma_subtrees}
    If $t, s \in \IPT(r, w)$ and $\exists p \in Sub(t) \cup Sub(s)$ such that $\snorm{t}{q} = \snorm{s}{q} \; \forall q \leq p$,
    then $\exists \widetilde{r}, \widetilde{w} : t|_p, s|_p \in \IPT(\widetilde{r}, \widetilde{w})$.
    \\
    Proof.
    By induction on position $p$.
    \\[-1em]

    Induction basis: the case of $p = \Lambda$ is trivial: let $\widetilde{r} = r$, $\widetilde{w} = w$.
    \\[-1em]

    Induction step: we have $|p| > 0$, let $p = p'.i$, where $i \in \YN$.
    Let $t' = t|_{p'} = T(t_1, \dots, t_n)$,
        $s' = s|_{p'} = T(s_1, \dots, s_m)$.
    By induction hypothesis $\exists r', w' : t', s' \in \IPT(r', w')$,
    where $w' = str(t_1) \dots str(t_n) = str(s_1) \dots str(s_m)$.
    \\[-1em]

    Next, we show that $str(t_i) = str(s_i)$.
    It must be that $i \in Sub(s') \cap Sub(t')$,
    otherwise only one of $\|t'\|_i$, $\|s'\|_i$ is $\infty$,
    which contradicts lemma condiiton $\|t\|_p = \|s\|_p$.
    Consider position $j \leq i$.
    Because the set of submatch positions contains siblings, we have $j \in Sub(s') \cap Sub(t')$.
    Consequently, $\|t'\|_j = |str(t_j)|$ and $\|s\|_j = |str(s_j)|$.
    By lemma condition we have $\|t\|_{p'.j} = \|s\|_{p'.j}$,
    therefore $\|t'\|_j = \|s'\|_j$,
    therefore $|str(t_j)| = |str(s_j)|$.
    Because $str(t_1) \dots str(t_n) = str(s_1) \dots str(s_m)$,
    we have $str(t_i) = str(s_i)$.
    \\[-1em]

    Now, let $\widetilde{w} = str(t_i)$.
    If $r' = r_1|r_2$ or $r' = r_1 r_2$, let $\widetilde{r} = r_i$.
    Otherwise, $r' = r_1^{k,l}$, let $\widetilde{r} = r_1$.
    $\square$
    \end{XLem}


    Proof of theorem \ref{theorem_order_compat}.
    \\[-1em]

    Consider any $t \in T_{min}$.
    For each position $p \in Sub(t)$, which is not itself a prefix of another position in $Sub(t)$,
    consider subtree $t' = t|_p$.
    It is an IPT for some sub-IRE $r'$ and substring $w'$: $t' \in \IPT(r', w')$.
    Let $t''$ be the $<$-minimal tree in $\IPT(r', w')$ and substitute $t'$ with $t''$ in $t$.
    (Note that substitutions are independent and can be performed in any order.)
    Let $u$ be the tree resulting from all such substitutions.
    By lemma \ref{incomparability_equivdef} we have $u \sim t$
    (because substitutions preserve the s-norm of subtrees at positions in $Sub(t)$),
    and so $u \in T_{min}$.
    We will show that $u = t_{min}$.
    \\[-1em]

    Suppose, on the contrary, that $u \neq t_{min}$.
    %
    Then we have $t_{min} <_p u$ for some non-submatch decision position $p$.
    Let $p = p'.p''$, where $p'$ is the longest prefix of $p$ that is a submatch position: $p' \in Sub(u) \cup Sub(t_{min})$.
    \\[-1em]

    It must be that for all submatch positions $q' < p'$ we have $\snorm{u}{q'} = \snorm{t_{min}}{q'}$,
    because $u \in T_{min}$ and thus either $u \sim t_{min}$,
    or $u \prec_q t_{min}$ for some $q \in Sub(u) \cup Sub(t_{min})$
    (in which case it must be $q > p$, because $u \prec_q t_{min}$ implies $\snorm{u}{q} > \snorm{t_{min}}{q}$,
    which in turn implies $\pnorm{u}{q} > \pnorm{t_{min}}{q}$,
    which contradicts $t_{min} <_p u$ if $q \leq p$).
    \\[-1em]

    Therefore by lemma \ref{lemma_subtrees} we have $\exists r', w' : u|_{p'}, t_{min}|_{p'} \in \IPT(r', w')$.
    On one hand, $t_{min} <_{p'.p''} u$ implies $t_{min}|_{p'} <_{p''} u|_{p'}$.
    But on the other hand, $p' \in Sub(u)$ and $p'$ is not itself a prefix of another position in $Sub(u)$,
    therefore $u|_{p'}$ is $<$-minimal by construction of $u$.
    Contradiction.
%    
%    %
%    On one hand, $u <_q \widetilde{s}$ for some submatch position $q$ (because $u \in P_{min}$).
%    On the other hand, $s \lessdot_p \widetilde{u}$ for some non-submatch position $p < q$ (because $s$ is $\lessdot$-minimal).
%    %
%    Let $p = p'.p''$, where $p'$ is the longest prefix of $p$ in $Sub(\widetilde{s}) \cup Sub(u)$.
%    It must be $\|u\|_{q'} = \|\widetilde{s}\|_{q'} \forall q' \leq p'$ (because $p' < q$ and $u <_q \widetilde{s}$),
%    and $p' \in Sub(u)$ (otherwise $\|u\|_{p'} = \infty \neq \|\widetilde{s}\|_{p'}$).
%    %
%    Now, by lemma \ref{lemma_subtrees} we have $\exists r', w' : u|_{p'}, \widetilde{s}|_{p'} \in PT(r', w')$,
%    therefore $s \lessdot_{p'.p''} u$ implies $s|_{p'} \lessdot_{p''} \widetilde{u}|_{p'}$.
%    But $p' \in Sub(u)$ and $p'$ is not itself a prefix of another position in $Sub(u)$,
%    therefore $\widetilde{u}|_{p'}$ is $\lessdot$-minimal by construction of $u$.
%    Contradiction.
    $\square$


\subsection*{Proof of Theorem \ref{theorem_order_on_pe_same_as_on_pt}}

    \begin{XLem}\label{lemma_pe_order_antisymm}
    The longest-leftmost-precedence relation $<$ is antisymmetric:
    if $\alpha < \beta$, then $\beta \not< \alpha$.
    \\
    Proof.
    Suppose, on the contrary, that $\alpha < \beta$ and $\beta < \alpha$.
    Let $\big( (\rho_0, \dots, \rho_n), (\rho'_0, \dots, \rho'_n) \big) = traces(\alpha, \beta)$.

    \medskip

    If $\exists i = max \{j \mid \rho_j \neq \rho'_j \}$, then
    $\alpha < \beta \implies \alpha \sqsubset \beta \implies \rho_i > \rho'_i$, but
    $\beta < \alpha \implies \beta \sqsubset \alpha \implies \rho'_i > \rho_i$. Contradiction.

    \medskip

    Otherwise $\rho_i = \rho'_i \; \forall i$, then
    $\alpha < \beta \implies \alpha \sim \beta \wedge \alpha \subset \beta$ and
    $\beta < \alpha \implies \beta \sim \alpha \wedge \beta \subset \alpha$.
    Let
    $x = first (\alpha \backslash \beta)$,
    $y = first (\beta \backslash \alpha)$, then
    $\alpha \subset \beta \implies x < y$, but
    $\beta \subset \alpha \implies y < x$. Contradiction.
    $\square$
    \end{XLem}


    \begin{XLem}\label{lemma_pe_equiv}
    Let $s, t \in PT(r, w)$.
    If $s \sim t$, then $\Phi_{h}(s) = \Phi_{h}(t) \; \forall h$.
    \\
    Proof.
    By induction on the height of $r$.

    \medskip

    Induction basis.
    For RT of height $1$ we have
    $| PT(r, w) | \leq 1 \; \forall w$,
    therefore $s = t$ and $\Phi_{h}(s) = \Phi_{h}(t)$.

    \medskip

    Induction step.
    We have
    $s = T^{d} (s_1, \dots, s_n)$ and
    $t = T^{d} (t_1, \dots, t_m)$.
    If $d = 0$, then $\Phi_{h}(s) = str(s) = w = str(t) = \Phi_{h}(t)$.
    Otherwise $d \neq 0$.
    By lemma \ref{incomparability_equivdef} we have $s \sim t \Rightarrow \forall p: \|s\|_p = \|t\|_p$.
    This implies $n = m$ (otherwise the norm of subtree at position $min(n,m)+1$ is $\infty$ for only one of $s$, $t$).
    Therefore
    $\Phi_{h}(s) = \Xl_{h+1} \Phi_{h+1}(s_1), \dots, \Phi_{h+1}(s_n) \Xr_h$ and
    $\Phi_{h}(t) = \Xl_{h+1} \Phi_{h+1}(t_1), \dots, \Phi_{h+1}(t_n) \Xr_h$.
%    Consider any $i \leq n$.
    It suffices to show that $\forall i \leq n: \Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$.
    We have $\forall p: \|s_i\|_p = \|t_i\|_p$ (implied by $\forall p: \|s\|_p = \|t\|_p$),
    therefore by lemma \ref{incomparability_equivdef} we have $s_i \sim t_i$,
    and by lemma \ref{lemma_subtrees} $\exists r', w': s_i, t_i \in PT(r', w')$,
    where the height of $r'$ is less than the height of $r$.
    By induction hypothesis $\Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$.
    $\square$
    \end{XLem}


    \begin{XLem}\label{lemma_pe_less_1}
    Let $s, t \in PT(r, w)$.
    If $s <_p t$ and $|p| = 1$, then $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$.
    \\
    Proof.

    By lemma conditions $|p| = 1$, which implies that $s$ and $t$ are compound PT
    $s = T^{d} (s_1, \dots, s_n)$ and 
    $t = T^{d} (t_1, \dots, t_m)$, where
    $d \neq 0$
    (because $\Lambda$ is a prefix of decision position $p$).
    Therefore $\Phi_{h}(s)$, $\Phi_{h}(t)$ can be represented as follows,
    where $k$ is the number of frames and $j$ is the fork:
    \begin{alignat*}{7}
        \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_n) \Xr_h
            &&\;=\; \beta_0 a_1 \dots a_j \beta_j &&\;\big|\; && \gamma_j a_{j + 1} \dots a_k \gamma_k \\[-0.5em]
        \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_m) \Xr_h
            &&\;=\; \beta_0 a_1 \dots a_j \beta_j &&\;\big|\; && \delta_j a_{j + 1} \dots a_k \delta_k
    \end{alignat*}
%
    By lemma conditions $|p| = 1$, therefore $p \in \YN$.
    Consider any $i \in \YN$ such that $i < p$.
    By lemma conditions $s <_p t$, which means
    $\|s\|_p > \|t\|_p \wedge \|s\|_q = \|t\|_q \;\forall q < p$.
    In particular $\|s_i\|_q = \|t_i\|_q \;\forall q$,
    therefore by lemma \ref{incomparability_equivdef} $s_i \sim t_i$
    and by lemma \ref{lemma_pe_equiv} we have $\Phi(s_i) = \Phi(t_i)$.
    Let $traces (\Phi_{h}(s), \Phi_{h}(t)) = \big( (\rho_0, \dots, \rho_k), (\rho'_0, \dots, \rho'_k) \big)$
    and consider the following cases.

    \medskip

    First case:
    $\infty = \|s_p\| > \|t_p\|$.
    In this case $s|_p$ does not exist
    (because $p$ corresponds to a submatch position in $r$,
    therefore $p \in Pos(s)$ implies $p \in Sub(s)$,
    which contradicts $\|s_p\| = \infty$).
    Fork happens immediately after $\Phi_{h+1}(s_{p-1})$, $\Phi_{h+1}(t_{p-1})$:
    \begin{alignat*}{7}
        \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1})
            &&\;\big|\; \Xr_{h}         &&      && \\[-0.5em]
        \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1})
            &&\;\big|\; \Phi_{h+1}(t_p) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h}
    \end{alignat*}
    %
    In this case fork frame is the last frame: $j = k$, and therefore $\rho_j = \rho'_j = h$
    (because $\gamma_j$ and $\delta_j$ contain the closing parenthesis $\Xr_{h}$).
    For all $i < j$ we have $\rho_i = \rho'_i = -1$, therefore $\Phi_{h}(s) \sim \Phi_{h}(t)$.
    Furthermore, $first(\gamma_j)$ is $\Xr$ and $first(\delta_j)$ is one of $\Xl$ and $\Xm$,
    therefore $\Phi_{h}(s) \subset \Phi_{h}(t)$.
    Consequently $\Phi_{h}(s) < \Phi_{h}(t)$.

    \medskip

    Second case: $\infty > \|s_p\| > \|t_p\| = -1$.
    In this case both $s_p$ and $t_p$ exist,
    $s_p$ is not $\varnothing$ and $t_p$ is $\varnothing$,
    and fork happens immediately after $\Phi_{h+1}(s_{p-1})$, $\Phi_{h+1}(t_{p-1})$:
    \begin{alignat*}{8}
        \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1})
            &&\;\big|\; \Xl_{h+1} \; x \; \Xr_{h+1} \; &&\Phi_{h+1}(s_{p+1}) &&\dots &&\Phi_{h+1}(s_n) \Xr_{h} \\[-0.5em]
        \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1})
            &&\;\big|\; \Xm_{h+1} \;\;\;\;\;\;         &&\Phi_{h+1}(t_{p+1}) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h}
    \end{alignat*}
    %
    If $j$-th frame is the last, we have $\rho_j = \rho'_j = h$ like in the first case.
    Otherwise we have $\rho_j = \rho'_j = h + 1$,
    because $minh(\gamma_j)$, $minh(\delta_j) \geq h + 1$
    and $lasth (\beta_j) = h + 1$
    (because if $p = 1$ then $\beta_j = \Xl_{h+1}$, otherwise
    $s_{p-1}$ exists and the last parenthesis in $\beta_j$
    is last parenthesis of $\Phi_{h+1}(s_{p-1})$, which is either $\Xr_{h+1}$ or $\Xm_{h+1}$).
    For subsequent frames $i$ such that $j < i < k$ we have $\rho_i = \rho'_i = h + 1$
    (because $minh(\gamma_j)$, $minh(\delta_j) \geq h + 1$),
    and for the last pair of frames we have $\rho_k = \rho'_k = h$.
    So in this case again $\Phi_{h}(s) \sim \Phi_{h}(t)$.
    Furthermore, $first (\gamma_j) = \Xl < \Xm = first (\delta_j)$, therefore $\Phi_{h}(s) \subset \Phi_{h}(t)$
    and $\Phi_{h}(s) < \Phi_{h}(t)$.

    \medskip

    Third case: $\infty > \|s_p\| > \|t_p\| \geq 0$.
    In this case both $s_p$ and $t_p$ exist and none of them is $\varnothing$,
    and fork happens somewhere after the opening parenthesis $\Xl$
    and before the closing parenthesis $\Xr$ in $\Phi_{h}(s_p)$, $\Phi_{h}(t_p)$:
    \begin{alignat*}{9}
        \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1}) &&\; \Xl_{h+2} \; x
            &&\;\big|\; y \; \Xr_{h+1} \; &&\Phi_{h+1}(s_{p+1}) &&\dots &&\Phi_{h+1}(s_n) \Xr_{h} \\[-0.5em]
        \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1}) &&\; \Xl_{h+2} \; x
            &&\;\big|\; z \; \Xr_{h+1} \; &&\Phi_{h+1}(t_{p+1}) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h}
    \end{alignat*}
    %
    Let $l$ be an index such that the frame $\delta_l$ contains the closing parenthesis $\Xr_{h+1}$ of $\Phi_{h+1}(t_p)$.
    It must be $l \geq j$ (equality is possible due to non-fully parenthesized expressions,
    as in the example $(a|aa)^{0,\infty}$ shown on figure \ref{fig_pe3}).
    Because $\|s_p\| > \|t_p\|$,
    the closing parenthesis $\Xr_{h+1}$ of $\Phi_{h+1}(s_p)$ is not contained in $\gamma_{l}$,
    and $l$-th frame is not the last one.
    Therefore $minh (\gamma_l) \geq h+2$ and $minh (\delta_l) = h+1$.
    Furthermore, $minh(x)$, $minh(y)$, $minh(z) \geq h + 2$,
    therefore $lasth(\beta_j) \geq h+2$ and
    for all frames $j \leq i < l$ (if such $i$ exist) we have $\rho_i, \rho'_i \geq h+2$
    (note that it might be $\rho_i < \rho'_i$).
    For the $l$-th frame $\rho_l \geq h+2 > h+1 = \rho'_l$.
    For subsequent frames $\gamma_i$, $\delta_i$ such that $l < i < k$ we have
    $minh(\gamma_i)$, $minh(\delta_i) \geq h + 1$,
    therefore $\rho_i \geq h+1 = \rho'_i$.
    For the last pair of frames $\rho_k = \rho'_k = h$.
    Therefore in this case $\Phi_{h}(s) \sqsubset \Phi_{h}(t)$,
    which implies $\Phi_{h}(s) < \Phi_{h}(t)$.
    $\square$
    \end{XLem}


    \begin{XLem}\label{lemma_pe_less}
    Let $s, t \in PT(r, w)$.
    If $s <_p t$, then $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$.
    \\
    Proof.
    By induction on the length of $p$.

    \medskip

    Induction basis for $|p| = 1$ is given by lemma \ref{lemma_pe_less_1}.

    \medskip

    Induction step.
    Let $|p| \geq 2$, then $s$ and $t$ are compound PT
    $s = T^{d} (s_1, \dots, s_n)$ and
    $t = T^{d} (t_1, \dots, t_m)$, where
    $d \neq 0$ (because $\Lambda$ is a prefix of decision position $p$).
    %
    Furthermore, let $p = p'.p''$, where $p' \in \YN$.
    Subtrees $s' = s_{p'}$ and $t' = t_{p'}$ exist, because $p'$ a proper prefix of decision position $p$,
    and they also must be compount PT
    $s' = T^{d'} (s'_1, \dots, s'_{n'})$ and
    $t' = T^{d'} (t'_1, \dots, t'_{m'})$,
    because $|p''| > 0$, and it must be
    $d' \neq 0$ (because $p'$ is a prefix of decision position $p$).
    %
    For subtrees $s_i$ and $t_i$ where $i < p'$ we have
    $\|s_i\|_q = \|t_i\|_q \;\forall q$ (implied by $s <_p t$),
    therefore by lemma \ref{incomparability_equivdef}
    $s_i \sim t_i$, and by lemma \ref{lemma_pe_equiv} we have $\Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$.
    %
    Therefore $\Phi_{h}(s)$, $\Phi_{h}(t)$ can be represented as follows:
    \begin{alignat*}{9}
        \Phi_{h}(s)
            \;&=
                \;&& \Xl_{h+1} \Phi_{h+1}(s_1) \dots \Phi_{h+1}(s_{p'-1})
                \;&& \overbrace {\Xl_{h+2} \Phi_{h+2}(s'_1) \dots \Phi_{h+2}(s'_{n'}) \Xr_{h+1}}^{\Phi_{h+1}(s')}
                \;&& \Phi_{h+1}(s_{p'+1}) \Phi_{h+1}(s_n) \Xr_{h}
                \\
        \Phi_{h}(t)
            \;&=
                \;&& \Xl_{h+1} \Phi_{h+1}(t_1) \dots \Phi_{h+1}(t_{p'-1})
                \;&& \underbrace {\Xl_{h+2} \Phi_{h+2}(t'_1) \dots \Phi_{h+2}(t'_{m'}) \Xr_{h+1}}_{\Phi_{h+1}(t')}
                \;&& \Phi_{h+1}(t_{p'+1}) \Phi_{h+1}(t_m) \Xr_{h}
    \end{alignat*}

    We have $\|s\|_q = \|t\|_q \;\forall q < p'$ (implied by $s <_p t$),
    therefore by lemma \ref{lemma_subtrees} $\exists r', w' : s', t' \in PT(r', w')$.
    Moreover, $s' <_{p''} t'$ and $|p''| < |p|$, therefore by induction hypothesis $\Phi_{p+1}(s') < \Phi_{p+1}(t')$.
    %
    On the other hand, if $j$ is the fork and $f \leq j \leq k$ then
    $\Phi_{h}(s)$, $\Phi_{h}(t)$ can be represented as:
    \begin{alignat*}{9}
        \Phi_{h}(s)
            \;&=
                \;&& \beta_0 a_1 \dots a_f \beta_f^1
                \;&& \overbrace {\beta_f^2  a_{f+1} \dots a_j \beta_j \;\big|\; \gamma_j a_{j+1} \dots a_k \gamma_k^1}^{\Phi_{h+1}(s')}
                \;&& \gamma_k^2 a_{k+1} \dots a_l \gamma_l
                \\[-0.5em]
        \Phi_{h}(t)
            \;&=
                \;&& \beta_0 a_1 \dots a_f \beta_f^1
                \;&& \underbrace {\beta_f^2  a_{f+1} \dots a_j \beta_j \;\big|\; \delta_j a_{j+1} \dots a_k \delta_k^1}_{\Phi_{h+1}(t')}
                \;&& \delta_k^2 a_{k+1} \dots a_l \delta_l
    \end{alignat*}

%    \begin{alignat*}{9}
%        \Phi_{h}(s)
%            \;&=
%                \;&&\overbrace  {\Xl_{h+1} \Phi_{h+1}(s_1) \dots \Phi_{h+1}(s_{p'-1})}
%                    ^{\beta_0 a_1 \dots a_i \beta_i^1}
%                \;&&\overbrace  {\Xl_{h+2} \Phi_{h+2}(s'_1) \dots \Phi_{h+2}(s'_{n'}) \Xr_{h+1}}
%                    ^{\beta_i^2  a_{i+1} \dots a_j \beta_j \;\big|\; \gamma_j a_{j+1} \dots a_k \gamma_k^1}
%                \;&&\overbrace  {\Phi_{h+1}(s_{p'+1}) \Phi_{h+1}(s_n) \Xr_{h}}
%                    ^{\gamma_k^2 a_{k+1} \dots a_l \gamma_l}
%                \\
%        \Phi_{h}(t)
%            \;&=
%                \;&&\underbrace {\Xl_{h+1} \Phi_{h+1}(t_1) \dots \Phi_{h+1}(t_{p'-1})}
%                    _{\beta_0 a_1 \dots a_i \beta_i^1}
%                \;&&\underbrace {\Xl_{h+2} \Phi_{h+2}(t'_1) \dots \Phi_{h+2}(t'_{m'}) \Xr_{h+1}}
%                    _{\beta_i^2  a_{i+1} \dots a_j \beta_j \;\big|\; \delta_j a_{j+1} \dots a_k \delta_k^1}
%                \;&&\underbrace {\Phi_{h+1}(t_{p'+1}) \Phi_{h+1}(t_m) \Xr_{h}}
%                    _{\delta_k^2 a_{k+1} \dots a_l \delta_l}
%    \end{alignat*}

    Let $traces (\Phi_{h}(s), \Phi_{h}(t)) = \big( (\rho_0, \dots, \rho_l), (\rho'_0, \dots, \rho'_l) \big)$
    and $traces (\Phi_{h+1}(s'), \Phi_{h+1}(t')) = \big( (\sigma_h, \dots, \sigma_k), (\sigma'_h, \dots, \sigma'_k) \big)$.
    %
    We show that for frames $i$ such that $j \leq i < k$ we have
    $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$,
    and for subsequent frames $k \leq i \leq l$ we have $\rho_i = \rho'_i$.

    \medskip

    First case: $i = j \leq k \leq l$ (the fork frame).
    Because $\Phi_{h+1}(s')$ and $\Phi_{h+1}(t')$ have nonempty common prefix $\Xl_{h+2}$,
    we have $lasht (\Phi_{h}(s) \sqcap \Phi_{h}(t)) = lasth (\Phi_{h+1}(s') \sqcap \Phi_{h+1}(t')) \geq h + 2$.
    %
    If $j < k$ then $minh (\gamma_j)$, $minh (\delta_j)$ are not affected by appending
    $\gamma^2_k$, $\delta^2_k$ and therefore $\rho_j = \sigma_j \wedge \rho'_j = \sigma'_j$.
    %
    Else if $j = k < l$ then we have $minh (\gamma^1_k) = minh (\delta^1_k) = h + 1$ and
    $minh (\gamma^2_k) = minh (\delta^2_k) \geq h + 1$, and
    therefore $\rho_j = \rho'_j = h + 1$.
    %
    Finally, if $j = l$ then $minh (\gamma_j) = minh (\delta_j) = h$ and $\rho_j = \rho'_j = h$.

    \medskip

    Second case: $j < i < k$.
    In this case the calculation of $\rho_i$, $\rho'_i$ depends on $\rho_j$, $\rho'_j$
    (for which we have shown $\rho_j = \sigma_j \wedge \rho'_j = \sigma'_j$) and
    is not affected by the appended $\gamma^2_k$, $\delta^2_k$, therefore
    $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$.

    \medskip

    Third case: $j < i = k < l$. We have
    $minh (\gamma^1_k) = minh (\delta^1_k) = h + 1$ and
    $minh (\gamma^2_k) = minh (\delta^2_k) \geq h + 1$,
    and none of the preceding frames after the fork contain parentheses with height less than $h + 1$,
    therefore $\rho_k = \rho'_k = h + 1$.

    \medskip

    Fourth case: $k < i < l$.
    We have $\rho_i = \rho'_i = h + 1$,
    because $\rho_k = \rho'_k = h + 1$ and $minh(\gamma_i)$, $minh(\delta_i) \geq h + 1$.

    \medskip

    Fifth case: $i = l$.
    We have $\rho_l = \rho'_l = h$.

    \medskip

    So, we have shown that $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$ for $j \leq i < k$
    and $\rho_i = \rho'_i$ for $k \leq i \leq l$.
    It trivially follows that $\Phi_{h+1}(s') \sqsubset \Phi_{h+1}(t')$ implies $\Phi_{h}(s) \sqsubset \Phi_{h}(t)$, and
    $\Phi_{h+1}(s') \sim \Phi_{h+1}(t')$ implies $\Phi_{h}(s) \sim \Phi_{h}(t)$.
    Because none of $\Phi_{h+1}(s')$, $\Phi_{h+1}(t')$ is a proper prefix of another,
    $\Phi_{h+1}(s') \subset \Phi_{h+1}(t')$ implies $\Phi_{h}(s) \subset \Phi_{h}(t)$.
    Therefore $\Phi_{h+1}(s') < \Phi_{h+1}(t')$ implies $\Phi_{h}(s) < \Phi_{h}(t)$.
    $\square$
    \end{XLem}


    Proof of theorem \ref{theorem_order_on_pe_same_as_on_pt}.
    \\[-1em]

    $\Rightarrow$. Given by lemma \ref{lemma_pe_less}.
    \\[-1em]

    $\Leftarrow$.
    We have $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$.
    Suppose that $\nexists p: s <_p t$.
    By lemma \ref{lemma_pe_order_antisymm} either $s = t$
    (in which case $\Phi_{h}(s) = \Phi_{h}(t)$, contradiction)
    or $t <_q s$ for some $q$
    (in which case $\Phi_{h}(t) < \Phi_{h}(s)$ by lemma \ref{lemma_pe_less}, contradiction).
    Therefore $\exists p: s <_p t$.
    $\square$


\end{document}

